Fixes for Coq 8.17+rc1 version

Author: mattam82

.github/workflows/build.yml

@@ -8,6 +8,7 @@ on:
       - 8.13
       - 8.12
       - 8.11
+      - 8.17
 
   pull_request: # On all pull-request changes
   release: # At release time
@@ -21,10 +22,10 @@ jobs:
     strategy:
       matrix:
         coq_version: 
-          - 'dev'
+          - '8.17'
         ocaml_version:
           - '4.09-flambda'
-        target: [ local, hott, dune ]
+        target: [ local ] # dune, hott left out for now waiting for HoTT package
       fail-fast: false
 
     steps:

coq-equations.opam

@@ -1,5 +1,5 @@
 opam-version: "2.0"
-version: "dev"
+version: "8.17.dev"
 authors: [ "Matthieu Sozeau <matthieu.sozeau@inria.fr>" "Cyprien Mangin <cyprien.mangin@m4x.org>" ]
 dev-repo: "git+https://github.com/mattam82/Coq-Equations.git"
 maintainer: "matthieu.sozeau@inria.fr"
@@ -31,7 +31,7 @@ run-test: [
   [make "test-suite"]
 ]
 depends: [
-  "coq" {= "dev"}
+  "coq" { >= "8.17~" & < "8.18" }
   "ocamlfind" {build}
 ]
 #depopts: [

src/covering.ml

@@ -30,7 +30,7 @@ type int_data = {
   flags : flags;
   program_mode : bool;
   intenv : Constrintern.internalization_env;
-  notations : Vernacexpr.notation_declaration list
+  notations : Vernacexpr.decl_notation list
 }
 
 exception Conflict
@@ -782,7 +782,7 @@ let interp_arity env evd ~poly ~is_rec ~with_evars notations (((loc,i),udecl,rec
   let program_sort =
     let u = Retyping.get_sort_of env !evd program_orig_type in
     let sigma, sortl, sortu = nonalgebraic_universe_level_of_universe env !evd u in
-    evd := sigma; ESorts.kind sigma sortu
+    evd := sigma; sortu
   in
   let program_implicits = Impargs.compute_implicits_with_manual env !evd program_orig_type false impls in
   let () = evd := Evd.minimize_universes !evd in
@@ -1509,7 +1509,7 @@ and interp_clause env evars p data prev clauses' path (ctx,pats,ctx' as prob)
          str "And clauses: " ++ pr_preclauses env !evars cls')
     | Some (clauses, s) ->
       let () = check_unused_clauses env !evars clauses in
-      let term, _ = term_of_tree env evars (ESorts.make p.program_sort) s in
+      let term, _ = term_of_tree env evars p.program_sort s in
       let info =
         { refined_obj = (idref, cconstr, cty);
           refined_rettyp = ty;
@@ -1531,7 +1531,7 @@ and interp_clause env evars p data prev clauses' path (ctx,pats,ctx' as prob)
 
 and interp_wheres env0 ctx evars path data s lets
     (ctx, envctx, liftn, subst)
-    (w : (pre_prototype * pre_equation list) list * Vernacexpr.notation_declaration list) =
+    (w : (pre_prototype * pre_equation list) list * Vernacexpr.decl_notation list) =
   let notations = snd w in
   let aux (data,lets,nlets,coverings,env)
       (((loc,id),udecl,nested,b,t,reca),clauses as eqs) =

src/covering.mli

@@ -75,7 +75,7 @@ type int_data = {
   flags : flags;
   program_mode : bool;
   intenv : Constrintern.internalization_env;
-  notations : Vernacexpr.notation_declaration list
+  notations : Vernacexpr.decl_notation list
 }
 
 val add_wfrec_implicits : Syntax.rec_type ->
@@ -246,7 +246,7 @@ val interp_arity : Environ.env ->
   poly:bool ->
   is_rec:bool ->
   with_evars:bool ->
-  Vernacexpr.notation_declaration list ->
+  Vernacexpr.decl_notation list ->
   pre_equation Syntax.where_clause ->
   program_info
 

src/depelim.ml

@@ -457,7 +457,7 @@ let dependent_elim_tac ?patterns id : unit Proofview.tactic =
     let program_orig_type = it_mkProd_or_LetIn ty ctx in
     let p = Syntax.{program_loc = default_loc;
                     program_id = Names.Id.of_string "dummy";
-                    program_orig_type; program_sort = (ESorts.kind sigma sort);
+                    program_orig_type; program_sort = sort;
                     program_impls = [];
                     program_implicits = [];
                     program_rec = None;

src/eqdec.ml

@@ -61,9 +61,9 @@ let inductive_info sigma ((mind, _ as ind),u) =
     let arities = arities_of_constructors env (from_peuniverses sigma induct) in
      let constrs =
       Array.map (fun ty -> 
-	let _, rest = decompose_prod_n_decls sigma nparams (EConstr.of_constr ty) in
+	let _, rest = decompose_prod_n_assum sigma nparams (EConstr.of_constr ty) in
 	let constrty = Vars.substl subst rest in
-	decompose_prod_decls sigma constrty)
+	decompose_prod_assum sigma constrty)
 	arities
     in
     let case c pred brs =

src/equations.mli

@@ -19,7 +19,7 @@ val define_by_eqs
   -> open_proof:bool
   -> Syntax.equation_options
   -> Syntax.pre_equations
-  -> Vernacexpr.notation_declaration list
+  -> Vernacexpr.decl_notation list
   -> Declare.OblState.t * Declare.Proof.t option
 
 val define_principles :
@@ -34,15 +34,15 @@ val equations :
   poly:bool -> program_mode:bool -> ?tactic:Libnames.qualid ->
   Syntax.equation_options ->
   Syntax.pre_equations ->
-  Vernacexpr.notation_declaration list ->
+  Vernacexpr.decl_notation list ->
   Declare.OblState.t
 
 val equations_interactive :
   pm:Declare.OblState.t ->
   poly:bool -> program_mode:bool -> ?tactic:Libnames.qualid ->
   Syntax.equation_options ->
   Syntax.pre_equations ->
-  Vernacexpr.notation_declaration list ->
+  Vernacexpr.decl_notation list ->
   Declare.OblState.t * Declare.Proof.t
 
 val solve_equations_goal :

src/equations_common.ml

@@ -42,7 +42,6 @@ let equations_derive_eliminator = ref true
 
 let _ = Goptions.declare_bool_option {
   Goptions.optdepr  = true;
-  Goptions.optstage = Interp;
   Goptions.optkey   = ["Equations"; "WithK"];
   Goptions.optread  = (fun () -> false);
   Goptions.optwrite = (fun b ->
@@ -55,47 +54,41 @@ let _ = Goptions.declare_bool_option {
 
 let _ = Goptions.declare_bool_option {
   Goptions.optdepr  = true;
-  Goptions.optstage = Interp;
   Goptions.optkey   = ["Equations"; "WithKDec"];
   Goptions.optread  = (fun () -> !simplify_withUIP);
   Goptions.optwrite = (fun b -> simplify_withUIP := b)
 }
 
 let _ = Goptions.declare_bool_option {
   Goptions.optdepr  = false;
-  Goptions.optstage = Interp;
   Goptions.optkey   = ["Equations"; "With"; "UIP"];
   Goptions.optread  = (fun () -> !simplify_withUIP);
   Goptions.optwrite = (fun b -> simplify_withUIP := b)
 }
 
 let _ = Goptions.declare_bool_option {
   Goptions.optdepr  = false;
-  Goptions.optstage = Interp;
   Goptions.optkey   = ["Equations"; "Transparent"];
   Goptions.optread  = (fun () -> !equations_transparent);
   Goptions.optwrite = (fun b -> equations_transparent := b)
 }
 
 let _ = Goptions.declare_bool_option {
   Goptions.optdepr  = false;
-  Goptions.optstage = Interp;
   Goptions.optkey   = ["Equations"; "With"; "Funext"];
   Goptions.optread  = (fun () -> !equations_with_funext);
   Goptions.optwrite = (fun b -> equations_with_funext := b)
 }
 
 let _ = Goptions.declare_bool_option {
   Goptions.optdepr  = false;
-  Goptions.optstage = Interp;
   Goptions.optkey   = ["Equations"; "Derive"; "Equations"];
   Goptions.optread  = (fun () -> !equations_derive_equations);
   Goptions.optwrite = (fun b -> equations_derive_equations := b)
 }
 
 let _ = Goptions.declare_bool_option {
   Goptions.optdepr  = false;
-  Goptions.optstage = Interp;
   Goptions.optkey   = ["Equations"; "Derive"; "Eliminator"];
   Goptions.optread  = (fun () -> !equations_derive_eliminator);
   Goptions.optwrite = (fun b -> equations_derive_eliminator := b)
@@ -107,7 +100,6 @@ let debug = ref false
 
 let _ = Goptions.declare_bool_option {
   Goptions.optdepr  = false;
-  Goptions.optstage = Interp;
   Goptions.optkey   = ["Equations"; "Debug"];
   Goptions.optread  = (fun () -> !debug);
   Goptions.optwrite = (fun b -> debug := b)
@@ -1076,19 +1068,19 @@ let evd_comb1 f evd x =
 (* Universe related functions *)
 
 let nonalgebraic_universe_level_of_universe env sigma u =
-  match ESorts.kind sigma u with
+  match u with
   | Sorts.Set | Sorts.Prop | Sorts.SProp ->
     sigma, Univ.Level.set, u
-  | Sorts.Type u0 | Sorts.QSort (_, u0) ->
+  | Sorts.Type u0 ->
     match Univ.Universe.level u0 with
     | Some l ->
       (match Evd.universe_rigidity sigma l with
       | Evd.UnivFlexible true ->
-        Evd.make_nonalgebraic_variable sigma l, l, ESorts.make @@ Sorts.sort_of_univ @@ Univ.Universe.make l
+        Evd.make_nonalgebraic_variable sigma l, l, Sorts.sort_of_univ @@ Univ.Universe.make l
       | _ -> sigma, l, u)
     | None ->
       let sigma, l = Evd.new_univ_level_variable Evd.univ_flexible sigma in
-      let ul = ESorts.make @@ Sorts.sort_of_univ @@ Univ.Universe.make l in
+      let ul = Sorts.sort_of_univ @@ Univ.Universe.make l in
       let sigma = Evd.set_leq_sort env sigma u ul in
       sigma, l, ul
 

src/equations_common.mli

@@ -400,7 +400,7 @@ val new_evar :            Environ.env ->
 val new_type_evar :            Environ.env ->
            Evd.evar_map -> 
            ?src:Evar_kinds.t Loc.located -> Evd.rigid ->
-           Evd.evar_map * (constr * ESorts.t)
+           Evd.evar_map * (constr * Sorts.t)
 
 val empty_hint_info : 'a Typeclasses.hint_info_gen
 
@@ -442,10 +442,10 @@ val splay_prod_n_assum : env -> Evd.evar_map -> int -> types -> rel_context * ty
 
 (* Universes *)
 val nonalgebraic_universe_level_of_universe :
-  Environ.env -> Evd.evar_map -> ESorts.t -> Evd.evar_map * Univ.Level.t * ESorts.t
+  Environ.env -> Evd.evar_map -> Sorts.t -> Evd.evar_map * Univ.Level.t * Sorts.t
 val instance_of :
   Environ.env ->
   Evd.evar_map ->
   ?argu:EConstr.EInstance.t ->
-  ESorts.t ->
-  Evd.evar_map * EConstr.EInstance.t * ESorts.t
+  Sorts.t ->
+  Evd.evar_map * EConstr.EInstance.t * Sorts.t

src/g_equations.mlg

@@ -199,7 +199,7 @@ let deppat_elim : Constrexpr.constr_expr list Pcoq.Entry.t =
 let _ = Pptactic.declare_extra_genarg_pprule wit_deppat_elim
   pr_raw_deppat_elim pr_glob_deppat_elim pr_deppat_elim
 
-type equations_argtype = (pre_equations * Vernacexpr.notation_declaration list) Genarg.uniform_genarg_type
+type equations_argtype = (pre_equations * Vernacexpr.decl_notation list) Genarg.uniform_genarg_type
 
 let wit_equations : equations_argtype =
   Genarg.create_arg "equations"
@@ -209,7 +209,7 @@ let pr_raw_equations _env _sigma _ _ _ l = mt ()
 let pr_glob_equations _env _sigma _ _ _ l = mt ()
 let pr_equations _env _sigma _ _ _ l = mt ()
 
-let equations : (pre_equations * Vernacexpr.notation_declaration list) Pcoq.Entry.t =
+let equations : (pre_equations * Vernacexpr.decl_notation list) Pcoq.Entry.t =
   Pcoq.create_generic_entry2 "equations" (Genarg.rawwit wit_equations)
 
 let _ = Pptactic.declare_extra_genarg_pprule wit_equations
@@ -332,8 +332,8 @@ GRAMMAR EXTEND Gram
     [ [ ntn = ne_lstring; ":="; c = constr;
         modl = G_vernac.syntax_modifiers;
         scopt = OPT [ ":"; sc = IDENT -> { sc } ] -> {
-        Inr { Vernacexpr.ntn_decl_string = ntn; ntn_decl_interp = c;
-              ntn_decl_modifiers = modl; ntn_decl_scope = scopt } }
+        Inr { Vernacexpr.decl_ntn_string = ntn; decl_ntn_interp = c;
+              decl_ntn_modifiers = modl; decl_ntn_scope = scopt } }
       | p = proto -> { Inl (p (Some Syntax.Nested)) } ] ]
   ;
 
@@ -357,8 +357,8 @@ GRAMMAR EXTEND Gram
     [ [ ntn = ne_lstring; ":="; c = constr;
         modl = G_vernac.syntax_modifiers;
         scopt = OPT [ ":"; sc = IDENT -> { sc } ] -> {
-        Inr { Vernacexpr.ntn_decl_string = ntn; ntn_decl_interp = c;
-              ntn_decl_modifiers = modl; ntn_decl_scope = scopt } }
+        Inr { Vernacexpr.decl_ntn_string = ntn; decl_ntn_interp = c;
+              decl_ntn_modifiers = modl; decl_ntn_scope = scopt } }
       | p = proto -> { Inl (p (Some Syntax.Mutual)) } ] ]
   ;
   local_where: