rename Qpoint_to_point into Qstraight_point_to_point

math-comp · Apr 30, 2024 · acac84a · acac84a
1 parent 96e7b3a
commit acac84a
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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