Chore: 9.1 compat

.github/workflows/ci.yml

@@ -12,7 +12,7 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        rocq: [ "9.2.0" ]
+        rocq: [ "9.1.1", "9.2.0" ]
       fail-fast: false
 
     steps:

Engine/PikeTree.v

@@ -17,7 +17,7 @@ From Linden Require Import Parameters BooleanSemantics Semantics.
 From Warblre Require Import Base RegExpRecord.
 
 (* Read, Progress, Choice, Reset *)
-Abbreviation lazy_iter c t1 t2 := (Read c (Progress (Choice t1 (GroupAction (Reset []) t2)))).
+Notation lazy_iter c t1 t2 := (Read c (Progress (Choice t1 (GroupAction (Reset []) t2)))).
 
 
 Section PikeTree.

Engine/Prefix.v

@@ -392,8 +392,8 @@ Variant literal : Type :=
 (* this indicates a match cannot exist, as opposed to Prefix [] which means we do not know anything about the match *)
 | Impossible.
 
-Abbreviation Nothing := (Exact []).
-Abbreviation Unknown := (Prefix []).
+Notation Nothing := (Exact []).
+Notation Unknown := (Prefix []).
 
 Definition literal_eq_dec: forall (l1 l2: literal), { l1 = l2 } + { l1 <> l2 }.
 Proof. decide equality; apply string_eq_dec. Defined.
@@ -586,7 +586,7 @@ Fixpoint extract_actions_literal (acts : list action) : literal :=
   | a :: rest => chain_literals (extract_action_literal a) (extract_actions_literal rest)
   end.
 
-Create Rewrite HintDb prefix.
+(* Create Rewrite HintDb prefix. *) (* LATER 9.2 *)
 Hint Unfold
   prefix
   chain_literals

Rewriting/Anchors.v

@@ -6,18 +6,18 @@ Section Anchors.
   Context {params: LindenParameters}.
   Context (rer: RegExpRecord).
 
-  Abbreviation ascii_word_canon :=
+  Notation ascii_word_canon :=
     (forall c,
         In c Character.ascii_word_characters ->
         In (Character.canonicalize rer c) Character.ascii_word_characters).
 
-  Abbreviation ascii_word_inall :=
+  Notation ascii_word_inall :=
     (forall c, In c Character.ascii_word_characters -> In c Character.all).
 
-  Abbreviation canonicalize_nonall_stable :=
+  Notation canonicalize_nonall_stable :=
     (forall c, In (Character.canonicalize rer c) Character.all <-> In c Character.all).
 
-  Abbreviation line_terminators_canon :=
+  Notation line_terminators_canon :=
     (forall c,
         In c Character.line_terminators <->
           In (Character.canonicalize rer c) Character.line_terminators).

Rewriting/Equivalence.v

@@ -223,7 +223,7 @@ Hint Unfold
   tree_nequiv_compute_dir
   : tree_equiv.
 
-Create Rewrite HintDb tree_equiv.
+(* Create Rewrite HintDb tree_equiv. *) (* LATER 9.2 *)
 Hint Rewrite app_nil_l app_nil_r : tree_equiv.
 Hint Rewrite <- app_assoc : tree_equiv.
 
@@ -264,7 +264,7 @@ Hint Unfold
      andb orb negb xorb
   : tree_equiv_symbex.
 
-Create Rewrite HintDb tree_equiv_symbex.
+(* Create Rewrite HintDb tree_equiv_symbex. *) (* LATER 9.2 *)
 Hint Rewrite
   PeanoNat.Nat.leb_le
   PeanoNat.Nat.leb_nle
@@ -295,7 +295,7 @@ Ltac leaves_equiv_step :=
 Ltac leaves_equiv_t :=
   first [ reflexivity | repeat leaves_equiv_step ].
 
-Create Rewrite HintDb charset.
+(* Create Rewrite HintDb charset. *) (* LATER 9.2 *)
 Hint Rewrite
   @CharSet.exist_canonicalized_equiv
   @CharSet.exist_spec

dune

@@ -4,5 +4,9 @@
  (name Linden)
  (package linden)
  (generate_project_file)
- (flags -set "Generate Goal Names")
+ (flags
+   ; LATER (9.2 only)
+   ; -set "Generate Goal Names"
+   -w -notation-for-abbreviation
+   -w -implicit-create-rewrite-hint-db)
  (theories Warblre Ltac2 Stdlib StrictOrderSolver))

dune-project

@@ -16,7 +16,7 @@
  (name linden)
  (synopsis "Formal Verification for JavaScript Regular Expressions")
  (depends
-  (rocq-core (>= 9.2.0))
+  (rocq-core (>= 9.1.1))
   (rocq-stdlib (>= 9.1.0))
   (warblre (= 0.1.0))
   (strict-order-solver (>= 1.0.0))))

linden.opam

@@ -8,7 +8,7 @@ homepage: "https://github.com/epfl-systemf/Linden"
 bug-reports: "https://github.com/epfl-systemf/Linden/issues"
 depends: [
   "dune" {>= "3.21"}
-  "rocq-core" {>= "9.2.0"}
+  "rocq-core" {>= "9.1.1"}
   "rocq-stdlib" {>= "9.1.0"}
   "warblre" {= "0.1.0"}
   "strict-order-solver" {>= "1.0.0"}