From 606a032690772729757f2809bcb4c150868bda28 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Wed, 24 Apr 2024 15:30:19 +0900
Subject: [PATCH] fix

---
 _CoqProject                   |  2 --
 html/Makefile                 | 11 -----------
 theories/extraction_command.v |  2 +-
 theories/no_crossing.v        |  2 +-
 4 files changed, 2 insertions(+), 15 deletions(-)
 delete mode 100644 html/Makefile

diff --git a/_CoqProject b/_CoqProject
index c03140a..a923345 100644
--- 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
deleted file mode 100644
index 07218d0..0000000
--- a/html/Makefile
+++ /dev/null
@@ -1,11 +0,0 @@
-all: Makefile.coq
-	make -f Makefile.coq
-
-Makefile.coq:
-	coq_makefile *.v -o Makefile.coq
-
-run:
-	python3 -m http.server
-
-clean:
-	make -f Makefile.coq clean
\ No newline at end of file
diff --git a/theories/extraction_command.v b/theories/extraction_command.v
index ab2c479..5c0ee72 100644
--- 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
index 0d81e85..2be8261 100644
--- 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)) &&