fix

math-comp · Apr 24, 2024 · 606a032 · 606a032
1 parent 495a956
commit 606a032
Show file tree

Hide file tree

Showing 4 changed files with 2 additions and 15 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -39,5 +39,3 @@ theories/smooth_trajectories.v
 
 -arg -w -arg -notation-overridden
 -arg -w -arg -ambiguous-paths
-theories/smooth_trajectories.v
-theories/generic_trajectories.v
diff --git a/html/Makefile b/html/Makefile
diff --git a/theories/extraction_command.v b/theories/extraction_command.v
@@ -1,4 +1,4 @@
-From trajectories Require Import smooth_trajectories.
+From trajectories Require Import generic_trajectories smooth_trajectories.
 Require Import QArith.
 
 Extraction "smooth_trajectories" smooth_point_to_point example_bottom example_top

diff --git a/theories/no_crossing.v b/theories/no_crossing.v
@@ -104,7 +104,7 @@ Definition have_crossing (e1 e2 : edge) : bool :=
   else
    (* The two edges are parallel.  They may still touch. *)
    if negb (Qeq_bool 
-             (area3 (left_pt e1) (left_pt e2) (right_pt e2)) 0) then
+             (area3 _ Qplus Qminus Qmult (left_pt e1) (left_pt e2) (right_pt e2)) 0) then
      true
    else
      (Qlt_bool (p_x (left_pt e2)) (p_x (left_pt e1)) &&