that one was easy!

uds-psl · Jan 30, 2024 · a7498ce · a7498ce
1 parent 89cb044
commit a7498ce
Show file tree

Hide file tree

Showing 5 changed files with 7 additions and 6 deletions.
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -10,7 +10,7 @@ jobs:
         opam_file:
           - 'coq-autosubst-ocaml.opam'
         image:
-          - 'coqorg/coq:8.18.0-ocaml-4.14.1-flambda' 
+          - 'coqorg/coq:8.19.0-ocaml-4.14.1-flambda' 
       fail-fast: false  # don't stop jobs if one fails
     steps:
       - uses: actions/checkout@v2

diff --git a/README.md b/README.md
@@ -14,7 +14,7 @@
 - Maintainer:
   - Yannick Forster ([**@yforster**](https://github.com/yforster))
 - License: [MIT License](LICENSE)
-- Compatible Coq versions: 8.18.0
+- Compatible Coq versions: 8.19.0
 - Related publication(s):
   - Adrian Dapprich's [bachelor thesis](https://www.ps.uni-saarland.de/~dapprich/bachelor.php) (Advisor: Andrej Dudenhefner, Supervisor: Gert Smolka)
 

diff --git a/coq-autosubst-ocaml.opam b/coq-autosubst-ocaml.opam
@@ -16,7 +16,7 @@ license: "MIT"
 
 depends: [
   "ocaml" { >= "4.09" & < "4.15" }
-  "coq" { >= "8.18.0" & < "8.19" }
+  "coq" { >= "8.19.0" & < "8.20" }
   "angstrom" { >= "0.15.0" }
   "dune" { >= "2.5" }
   "ocamlgraph" { >= "2.0.0" }

diff --git a/lib/automationGen.ml b/lib/automationGen.ml
@@ -51,6 +51,7 @@ module TacGen = struct
       rZeta = true;
       rDelta = delta;
       rConst = consts;
+      rStrength = Norm ;
     } in
     let cbn = Genredexpr.Cbn flags in
     (CAst.make (TacAtom (TacReduce (cbn, locus_clause))))

diff --git a/lib/gallinaGen.ml b/lib/gallinaGen.ml
@@ -15,9 +15,9 @@ let name_id_ s = Names.Id.of_string s
 let lident_ s = CAst.make (name_id_ s)
 let name_ s = Names.Name.mk_name (name_id_ s)
 
-let underscore_ = CAst.make Constrexpr.(CHole (None, Namegen.IntroAnonymous))
+let underscore_ = CAst.make Constrexpr.(CHole None)
 let prop_ = CAst.make Constrexpr.(CSort (Glob_term.UNamed (None,[CProp, 0])))
-let type_ = CAst.make Constrexpr.(CSort (Glob_term.UAnonymous { rigid = true }))
+let type_ = CAst.make Constrexpr.(CSort (Glob_term.UAnonymous { rigid = UnivRigid }))
 
 let app_ f xs =
   Constrexpr_ops.mkAppC (f, xs)
@@ -91,7 +91,7 @@ let match_ cexpr ?rtype bexprs =
 let binder_ ?(implicit=false) ?btype bnames =
   let open Constrexpr in
   let bk = Default (if implicit then Glob_term.MaxImplicit else Glob_term.Explicit) in
-  let btype = Option.default (CAst.make @@ CHole (None, Namegen.IntroAnonymous)) btype in
+  let btype = Option.default (CAst.make @@ CHole None) btype in
   CLocalAssum (List.map lname_ bnames, bk, btype)
 
 let binder1_ ?implicit ?btype bname =