Fixes for Coq 8.17+rc1 version

.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 <[email protected]>" "Cyprien Mangin <[email protected]>" ]
 dev-repo: "git+https://github.com/mattam82/Coq-Equations.git"
 maintainer: "[email protected]"
@@ -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:

src/noconf.ml

@@ -93,9 +93,9 @@ let derive_no_confusion ~pm env sigma0 ~poly (ind,u as indu) =
     | Sorts.InSProp -> mkSProp
     | Sorts.InProp -> mkProp
     | Sorts.InSet -> mkSet
-    | Sorts.InType | Sorts.InQSort ->
+    | Sorts.InType ->
       (* In that case the noConfusion principle lives at the level of the type. *)
-      let sort = EConstr.mkSort (ESorts.make inds) in
+      let sort = EConstr.mkSort inds in
       let sigma, s =
         Evarsolve.refresh_universes ~status:Evd.univ_flexible ~onlyalg:true
           (Some false) env !evd sort

src/noconf_hom.ml

@@ -132,11 +132,11 @@ let derive_no_confusion_hom ~pm env sigma0 ~poly (ind,u as indu) =
   let fullbinders = ydecl :: binders in
   let sigma, s =
     match Lazy.force logic_sort with
-    | Sorts.InType | Sorts.InSet | Sorts.InQSort -> (* In that case noConfusion lives at the level of the inductive family *)
-      let sort = EConstr.mkSort (ESorts.make inds) in
+    | Sorts.InType | Sorts.InSet -> (* In that case noConfusion lives at the level of the inductive family *)
+      let sort = EConstr.mkSort inds in
       let is_level = match inds with
       | Sorts.Prop | Sorts.SProp | Sorts.Set -> true
-      | Sorts.Type u | Sorts.QSort (_, u) -> Univ.Universe.is_level u
+      | Sorts.Type u -> Univ.Universe.is_level u
       in
       if is_level then sigma, sort
       else

src/principles.ml

@@ -305,7 +305,7 @@ let abstract_rec_calls sigma user_obls ?(do_subst=true) is_rec len protos c =
                hyps args
            in
            let fargs' = Constr.mkApp (f', Array.of_list fargs') in
-           let result = Termops.it_mkLambda_or_LetIn fargs' sign in
+           let result = Term.it_mkLambda_or_LetIn fargs' sign in
            let hyp =
              Term.it_mkProd_or_LetIn
                (Constr.mkApp (mkApp (mkRel (i + 1 + len + n + List.length sign), Array.of_list indargs'),
@@ -816,7 +816,7 @@ let subst_rec_programs env evd ps =
       let splitting' =
           aux rec_cutprob s' program' oterm path' p.program_splitting
       in
-      let term', ty' = term_of_tree env evd (ESorts.make prog_info.program_sort) splitting' in
+      let term', ty' = term_of_tree env evd prog_info.program_sort splitting' in
       { program_rec = None;
         program_info = program_info';
         program_prob = id_subst (pi3 cutprob_sign);
@@ -940,7 +940,7 @@ let subst_rec_programs env evd ps =
       let refarg = ref (0,0) in
       let refhead =
         if islogical then
-          let term', _ = term_of_tree env evd (ESorts.make p.program_info.program_sort) s' in
+          let term', _ = term_of_tree env evd p.program_info.program_sort s' in
           term'
          else mapping_constr !evd subst oterm
       in
@@ -1424,13 +1424,11 @@ let max_sort s1 s2 =
   | (Prop, (Set | Type _ as s)) | ((Set | Type _) as s, Prop) -> s
   | (Set, Type u) | (Type u, Set) -> Sorts.sort_of_univ (Univ.Universe.sup Univ.Universe.type0 u)
   | (Type u, Type v) -> Sorts.sort_of_univ (Univ.Universe.sup u v)
-  | (QSort _, _) | (_, QSort _) -> assert false
 
 let level_of_context env evd ctx acc =
   let _, lev =
     List.fold_right (fun decl (env, lev) ->
         let s = Retyping.get_sort_of env evd (get_type decl) in
-        let s = ESorts.kind evd s in
         (push_rel decl env, max_sort s lev))
                     ctx (env,acc)
   in lev
@@ -1647,7 +1645,7 @@ let build_equations ~pm with_ind env evd ?(alias:alias option) rec_info progs =
     let entry =
       Entries.{ mind_entry_typename = indid;
                 mind_entry_arity = to_constr !evd (it_mkProd_or_LetIn (mkProd (anonR, arity,
-                                                                               mkSort (ESorts.make ind_sort))) sign);
+                                                                               mkSort ind_sort)) sign);
                 mind_entry_consnames = consnames;
                 mind_entry_lc = constructors;
               }
@@ -1663,7 +1661,7 @@ let build_equations ~pm with_ind env evd ?(alias:alias option) rec_info progs =
                     mind_entry_lc = List.map (to_constr sigma) (List.map of_constr entry.mind_entry_lc);
                     mind_entry_arity =
                       to_constr sigma (it_mkProd_or_LetIn (mkProd (anonR, arity,
-                                                                  mkSort (ESorts.make sort))) sign) })
+                                                                  mkSort sort)) sign) })
         inds
     in
     let univs, ubinders = Evd.univ_entry ~poly sigma in

src/principles_proofs.ml

@@ -400,7 +400,7 @@ let aux_ind_fun info chop nested unfp unfids p =
                 arity, arg, r.wf_rec_rel
               in
               let _functional_type, functional_type, fix =
-                Covering.wf_fix_constr env evd inctx concl (ESorts.kind !evd sort) arity arg rel
+                Covering.wf_fix_constr env evd inctx concl sort arity arg rel
               in
               (* TODO solve WellFounded evar *)
               let sigma, evar = new_evar env !evd functional_type in