diff --git a/theories/smooth_trajectories.v b/theories/smooth_trajectories.v
index 2aa1993..8eb2669 100644
--- a/theories/smooth_trajectories.v
+++ b/theories/smooth_trajectories.v
@@ -45,7 +45,7 @@ Definition euclidean_distance  (p1x p1y p2x p2y : R) :=
 
 Definition pt_distance := euclidean_distance.
 
-Definition Qpoint_to_point :=
+Definition Qstraight_point_to_point :=
   point_to_point Q Qeq_bool Qle_bool Qplus Qminus Qmult Qdiv
    pt_distance 1 edge Bedge left_pt right_pt.
 
diff --git a/www/Makefile.coq.local b/www/Makefile.coq.local
index 86b4c69..3465d69 100644
--- a/www/Makefile.coq.local
+++ b/www/Makefile.coq.local
@@ -9,7 +9,7 @@ clean::
 
 
 SmoothTrajectories.ml SmoothTrajectories.mli : ../theories/smooth_trajectories.vo
-	cd ../theories; echo 'Require Import QArith smooth_trajectories. Extraction "SmoothTrajectories.ml" Qsmooth_point_to_point Qpoint_to_point Qedges_to_cells Qreduction.Qred.' | coqtop -R . trajectories
+	cd ../theories; echo 'Require Import QArith smooth_trajectories. Extraction "SmoothTrajectories.ml" Qsmooth_point_to_point Qstraight_point_to_point Qedges_to_cells Qreduction.Qred.' | coqtop -R . trajectories
 	cp ../theories/SmoothTrajectories.ml ../theories/SmoothTrajectories.mli .
 
 SmoothTrajectories.cmi : SmoothTrajectories.mli