Coq 8.20, rm infra.v, minor fixes

Author: affeldt-aist

_CoqProject

@@ -9,7 +9,6 @@ theories/civt.v
 theories/desc.v
 theories/desc1.v
 theories/desc2.v
-theories/infra.v
 theories/bern.v
 theories/bern5.v
 theories/casteljau.v

coq-mathcomp-trajectories.opam

@@ -17,7 +17,7 @@ TODO"""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.17" & < "8.20~") | (= "dev") }
+  "coq" { (>= "8.17" & < "8.21~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "2.2.0") | (= "dev") }
   "coq-mathcomp-fingroup" { (>= "2.2.0") | (= "dev") }
   "coq-mathcomp-algebra" { (>= "2.2.0") | (= "dev") }

meta.yml

@@ -28,7 +28,7 @@ license:
 
 supported_coq_versions:
   text: Coq >= 8.17, MathComp >= 2.2.0
-  opam: '{ (>= "8.17" & < "8.20~") | (= "dev") }'
+  opam: '{ (>= "8.17" & < "8.21~") | (= "dev") }'
 
 tested_coq_opam_versions:
 - version: '2.2.0-coq-8.19'

theories/cells_alg.v

@@ -4959,7 +4959,7 @@ Record common_invariant bottom top edge_set s
      lexePt (point (head dummy_event events)) (right_pt g)}
 }.
 
-Record common_non_gp_invariant bottom top edge_set s 
+Record common_non_gp_invariant bottom top edge_set s
   (all_events processed_events events : seq event) :=
   { ngcomm : common_invariant bottom top edge_set s all_events
     processed_events events;

theories/general_position.v

@@ -17,119 +17,119 @@ Section working_environment.
 
 Variable R : realFieldType.
 
-(* Notation prefix, dupplicated from cells_alg.v *)
-Notation pt := (pt (RealField.sort R)).
-Notation p_x := (p_x (RealField.sort R)).
-Notation p_y := (p_y (RealField.sort R)).
-Notation Bpt := (Bpt (RealField.sort R)).
+(* Notation prefix, duplicated from cells_alg.v *)
+Notation pt := (pt (Num.RealField.sort R)).
+Notation p_x := (p_x (Num.RealField.sort R)).
+Notation p_y := (p_y (Num.RealField.sort R)).
+Notation Bpt := (Bpt (Num.RealField.sort R)).
 Notation edge := (edge R).
 Notation left_pt := (@left_pt R).
 Notation right_pt := (@right_pt R).
-Notation event := (event (RealField.sort R) edge).
-Notation outgoing := (outgoing (RealField.sort R) edge).
-Notation point := (point (RealField.sort R) edge).
-Notation cell := (cell (RealField.sort R) edge).
+Notation event := (event (Num.RealField.sort R) edge).
+Notation outgoing := (outgoing (Num.RealField.sort R) edge).
+Notation point := (point (Num.RealField.sort R) edge).
+Notation cell := (cell (Num.RealField.sort R) edge).
 
-Notation dummy_pt := (dummy_pt (RealField.sort R) 1).
-Notation dummy_edge := (dummy_edge (RealField.sort R) 1 edge (@unsafe_Bedge _)).
+Notation dummy_pt := (dummy_pt (Num.RealField.sort R) 1).
+Notation dummy_edge := (dummy_edge (Num.RealField.sort R) 1 edge (@unsafe_Bedge _)).
 Notation dummy_cell :=
-  (dummy_cell (RealField.sort R) 1 edge (@unsafe_Bedge _)).
-Notation dummy_event := (dummy_event (RealField.sort R) 1 edge).
+  (dummy_cell (Num.RealField.sort R) 1 edge (@unsafe_Bedge _)).
+Notation dummy_event := (dummy_event (Num.RealField.sort R) 1 edge).
 Notation edge_below :=
-  (generic_trajectories.edge_below (RealField.sort R) eq_op <=%R +%R
+  (generic_trajectories.edge_below (Num.RealField.sort R) eq_op <=%R +%R
     (fun x y => x - y) *%R 1 edge left_pt right_pt).
 Notation "x <| y" := (edge_below x y).
 Notation valid_edge :=
-  (generic_trajectories.valid_edge (RealField.sort R)
+  (generic_trajectories.valid_edge (Num.RealField.sort R)
    le edge left_pt right_pt).
 Notation vertical_intersection_point :=
-  (vertical_intersection_point (RealField.sort R)
+  (vertical_intersection_point (Num.RealField.sort R)
   le +%R (fun x y => x - y) *%R
   (fun x y => x / y) edge left_pt right_pt).
 Notation point_under_edge :=
-  (point_under_edge (RealField.sort R) le +%R (fun x y => x - y) *%R 1
+  (point_under_edge (Num.RealField.sort R) le +%R (fun x y => x - y) *%R 1
   edge left_pt right_pt).
 Notation "p <<= g" := (point_under_edge p g).
 Notation "p >>> g" := (~~ (point_under_edge p g)).
 Notation point_strictly_under_edge :=
-  (point_strictly_under_edge  (RealField.sort R) eq_op <=%R +%R
+  (point_strictly_under_edge  (Num.RealField.sort R) eq_op <=%R +%R
   (fun x y => x - y) *%R 1 edge left_pt right_pt).
 Notation "p <<< g" := (point_strictly_under_edge p g).
 Notation "p >>= g" := (~~ (point_strictly_under_edge p g)).
 
 Notation contains_point :=
-  (contains_point (RealField.sort R) eq_op <=%R +%R (fun x y => x - y) *%R 1
+  (contains_point (Num.RealField.sort R) eq_op <=%R +%R (fun x y => x - y) *%R 1
     edge left_pt right_pt).
 
 Notation open_cells_decomposition_contact :=
-  (open_cells_decomposition_contact (RealField.sort R) eq_op le +%R
+  (open_cells_decomposition_contact (Num.RealField.sort R) eq_op le +%R
   (fun x y => x - y) *%R 1 edge left_pt right_pt).
 Notation open_cells_decomposition_rec :=
-  (open_cells_decomposition_rec (RealField.sort R) eq_op le +%R
+  (open_cells_decomposition_rec (Num.RealField.sort R) eq_op le +%R
   (fun x y => x - y) *%R 1 edge (@unsafe_Bedge R) left_pt
   right_pt).
 Notation open_cells_decomposition :=
-  (open_cells_decomposition (RealField.sort R) eq_op le +%R
+  (open_cells_decomposition (Num.RealField.sort R) eq_op le +%R
   (fun x y => x - y) *%R 1 edge (@unsafe_Bedge R) left_pt
   right_pt).
 
-Notation scan_state := (scan_state (RealField.sort R) edge).
-Notation sc_open1 := (sc_open1 (RealField.sort R) edge).
-Notation lst_open := (lst_open (RealField.sort R) edge).
-Notation sc_open2 := (sc_open2 (RealField.sort R) edge).
-Notation sc_closed := (sc_closed (RealField.sort R) edge).
-Notation lst_closed := (lst_closed (RealField.sort R) edge).
+Notation scan_state := (scan_state (Num.RealField.sort R) edge).
+Notation sc_open1 := (sc_open1 (Num.RealField.sort R) edge).
+Notation lst_open := (lst_open (Num.RealField.sort R) edge).
+Notation sc_open2 := (sc_open2 (Num.RealField.sort R) edge).
+Notation sc_closed := (sc_closed (Num.RealField.sort R) edge).
+Notation lst_closed := (lst_closed (Num.RealField.sort R) edge).
 
 Notation update_closed_cell :=
-  (update_closed_cell (RealField.sort R) 1 edge).
+  (update_closed_cell (Num.RealField.sort R) 1 edge).
 
 Notation set_left_pts :=
-  (set_left_pts (RealField.sort R) edge).
+  (set_left_pts (Num.RealField.sort R) edge).
 
-Notation low := (low (RealField.sort R) edge).
-Notation high := (high (RealField.sort R) edge).
-Notation left_pts := (left_pts (RealField.sort R) edge).
-Notation right_pts := (right_pts (RealField.sort R) edge).
-Notation Bcell := (Bcell (RealField.sort R) edge).
+Notation low := (low (Num.RealField.sort R) edge).
+Notation high := (high (Num.RealField.sort R) edge).
+Notation left_pts := (left_pts (Num.RealField.sort R) edge).
+Notation right_pts := (right_pts (Num.RealField.sort R) edge).
+Notation Bcell := (Bcell (Num.RealField.sort R) edge).
 Notation cell_center :=
-  (cell_center (RealField.sort R) +%R (fun x y => x / y) 1%:R edge).
+  (cell_center (Num.RealField.sort R) +%R (fun x y => x / y) 1%:R edge).
 
 Notation closing_cells :=
-  (generic_trajectories.closing_cells (RealField.sort R) eq_op <=%R +%R (fun x y => x - y)
+  (generic_trajectories.closing_cells (Num.RealField.sort R) eq_op <=%R +%R (fun x y => x - y)
     *%R (fun x y => x / y) edge left_pt right_pt).
 Notation close_cell :=
-  (generic_trajectories.close_cell (RealField.sort R) eq_op <=%R +%R (fun x y => x - y)
+  (generic_trajectories.close_cell (Num.RealField.sort R) eq_op <=%R +%R (fun x y => x - y)
     *%R (fun x y => x / y) edge left_pt right_pt).
 
-Notation set_pts := (set_pts (RealField.sort R) edge).
+Notation set_pts := (set_pts (Num.RealField.sort R) edge).
 
 (* This function is to be called only when the event is in the middle
   of the last opening cell.  The point e needs to be added to the left
   points of one of the newly created open cells, but the one that receives
   the first segment of the last opening cells should keep its existing
   left points.*)
 Notation update_open_cell :=
-  (update_open_cell (RealField.sort R) eq_op le +%R (fun x y => x - y)
+  (update_open_cell (Num.RealField.sort R) eq_op le +%R (fun x y => x - y)
   *%R (fun x y => x / y) 1 edge (@unsafe_Bedge R) left_pt right_pt).
 
 Notation update_open_cell_top :=
-  (update_open_cell_top (RealField.sort R) eq_op le +%R (fun x y => x - y)
+  (update_open_cell_top (Num.RealField.sort R) eq_op le +%R (fun x y => x - y)
   *%R (fun x y => x / y) 1
   edge (@unsafe_Bedge R) left_pt right_pt).
 
-Notation Bscan := (Bscan (RealField.sort R) edge).
+Notation Bscan := (Bscan (Num.RealField.sort R) edge).
 
 Notation opening_cells_aux :=
-  (opening_cells_aux (RealField.sort R) eq_op <=%R +%R (fun x y => x - y)
+  (opening_cells_aux (Num.RealField.sort R) eq_op <=%R +%R (fun x y => x - y)
   *%R (fun x y => x / y) 1 edge (@unsafe_Bedge R) left_pt right_pt).
 
 Notation simple_step :=
-  (generic_trajectories.simple_step (RealField.sort R) eq_op le +%R
+  (generic_trajectories.simple_step (Num.RealField.sort R) eq_op le +%R
   (fun x y => x - y) *%R (fun x y => x / y)
   1 edge (@unsafe_Bedge R) left_pt right_pt).
 
 Notation step :=
-  (step (RealField.sort R) eq_op le +%R (fun x y => x - y) *%R
+  (step (Num.RealField.sort R) eq_op le +%R (fun x y => x - y) *%R
   (fun x y => x / y) 1 edge (@unsafe_Bedge R) left_pt right_pt).
 (*
 Definition scan events st : seq cell * seq cell :=
@@ -138,7 +138,7 @@ Definition scan events st : seq cell * seq cell :=
    lst_closed final_state :: sc_closed final_state). *)
 
 Notation start_open_cell :=
-  (start_open_cell (RealField.sort R) eq_op le +%R (fun x y => x - y)
+  (start_open_cell (Num.RealField.sort R) eq_op le +%R (fun x y => x - y)
   *%R (fun x y => x / y) edge left_pt right_pt).
 
 Notation open_cell_side_limit_ok :=
@@ -1531,4 +1531,4 @@ have lo_lb' : {in state_open_seq rstate, forall c,
 by constructor.
 Qed.
 
-End working_environment.
+End working_environment.