Update Coq to 8.19

Common/CBase.v

@@ -159,26 +159,26 @@ Notation "(.× x )" := (λ y, cprod y x) (only parsing) : stdpp_scope.
 (** * Constrained quantifiers ***)
 
 #[local] Notation "∀in x ∈ b , P" := (∀ x, x ∈ b → P)
-  (at level 200, x binder, right associativity, only parsing) : type_scope.
+  (at level 10, x binder, only parsing, P at level 200) : type_scope.
 
 Notation "∀ x .. y ∈ b , P" := (∀in x ∈ b, .. (∀in y ∈ b, P) ..)
-  (at level 200, x binder, y binder, right associativity, only parsing) : type_scope.
+  (at level 10, x binder, y binder, only parsing, P at level 200) : type_scope.
 
 (* Due to https://github.com/coq/coq/issues/18318, We only reprint constrained
    quantifiers one by one, and not as a group. This allows to specify the proper
    "closed binder" printing specification *)
 Notation "∀ x ∈ b , P" := (∀ x, x ∈ b → P)
-  (at level 200, x closed binder, right associativity, only printing,
+  (at level 200, x closed binder, only printing,
     format "'[  ' '[  ' ∀  x  ∈  b ']' ,  '/' P ']'") : type_scope.
 
 #[local] Notation "∃in x ∈ b , P" := (∃ x, x ∈ b ∧ P)
-  (at level 200, x binder, right associativity , only parsing) : type_scope.
+  (at level 10, x binder, only parsing, P at level 200) : type_scope.
 
 Notation "∃ x .. y ∈ b , P" := (∃in x ∈ b, .. (∃in y ∈ b, P) ..)
-  (at level 200, x binder, y binder, right associativity, only parsing) : type_scope.
+  (at level 10, x binder, y binder, only parsing, P at level 200) : type_scope.
 
 Notation "∃ x ∈ b , P" := (∃ x, x ∈ b ∧ P)
-  (at level 200, x closed binder, right associativity, only printing,
+  (at level 10, x closed binder, only printing,
     format "'[  ' '[  ' ∃  x  ∈  b ']' ,  '/' P ']'") : type_scope.
 
 
@@ -257,7 +257,7 @@ Ltac2 revert_until (clr : bool) (p : pattern) :=
          | [] => if match_pat p c then [h] else []
          | l => h :: l
          end
-      ) (Control.hyps ()) []
+      ) [] (Control.hyps ())
 
   with
   | [] => Control.zero Not_found

Extraction/ArmInstExtr.v

@@ -3,5 +3,9 @@ Require Import GenModels.ArmSeqModel.
 
 Unset Extraction SafeImplicits.
 
+(* DO NOT run this file in your editor. This will extract in the correct folder
+   when dune does the extraction *)
+Set Extraction Output Directory ".".
+
 #[warnings="-extraction-remaining-implicit"]
 Separate Extraction sequential_modelc.

INSTALL.md

@@ -41,14 +41,16 @@ opam install dune
 
 ### Coq
 
-This project was tested with Coq 8.18.0. If you want exactly that version do:
+This project was tested with Coq 8.19.1. If you want exactly that version do:
 ```
-opam pin coq 8.18.0
+opam pin coq 8.19.2
 ```
 otherwise you can install it with `opam install coq`
 
-Until recently it was working on 8.14 and 8.16, but no guarantees are made to keep
-supporting them.
+Due to Ltac2 version we don't think it will work with lower version of Coq such
+as 8.18* and below. However modifications needed are probably minimal if you do
+need it. At the time of writing some dependencies are not ported yet to Coq 8.20
+and later.
 
 
 ### Sail
@@ -109,7 +111,7 @@ git clone https://github.com/rems-project/coq-sail
 
 Then (optionally), in that repository, if you want the version used for development, do:
 ```
-git checkout 51506978
+git checkout 562597f
 ```
 
 Then you can install `coq-sail-stdpp` with `opam pin coq-sail-stdpp .` in the

ISASem/ArmInst.v

@@ -308,14 +308,8 @@ Proof. solve_decision. Defined.
 #[global] Instance S2TTWParams_eq_dec : EqDecision S2TTWParams.
 Proof. solve_decision. Defined.
 
-Definition sigT_ArithFactP_eq_dec `{EqDecision A} (P : A → Prop) : EqDecision {x : A & ArithFactP (P x)}.
-Proof.
-  intros [x ?] [y ?]. destruct decide (x = y).
-  - left. abstract (subst; f_equal; apply proof_irrelevance).
-  - right. abstract naive_solver.
-Defined.
-
-#[global] Instance Level_eq_dec : EqDecision Level := sigT_ArithFactP_eq_dec _.
+#[global] Instance Level_eq_dec : EqDecision Level.
+Proof. solve_decision. Defined.
 
 #[global] Instance Regime_eq_dec : EqDecision Regime.
 Proof. solve_decision. Defined.