From 88845b8a453cc5886260ac84c41a7a9eb3011684 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 6 Jan 2023 16:22:14 +0100 Subject: [PATCH] Fixes for Coq 8.17+rc1 version --- .github/workflows/build.yml | 5 +++-- coq-equations.opam | 4 ++-- src/covering.ml | 8 ++++---- src/covering.mli | 4 ++-- src/depelim.ml | 2 +- src/eqdec.ml | 4 ++-- src/equations.mli | 6 +++--- src/equations_common.ml | 16 ++++------------ src/equations_common.mli | 8 ++++---- src/g_equations.mlg | 12 ++++++------ src/noconf.ml | 4 ++-- src/noconf_hom.ml | 6 +++--- src/principles.ml | 12 +++++------- src/principles_proofs.ml | 2 +- src/sigma_types.ml | 4 +--- src/simplify.ml | 2 +- src/simplify.mli | 2 +- src/splitting.ml | 10 +++++----- src/splitting.mli | 2 +- src/subterm.ml | 2 +- src/syntax.ml | 6 +++--- src/syntax.mli | 6 +++--- 22 files changed, 58 insertions(+), 69 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 6b1b08de..b3182e9f 100644 --- a/.github/workflows/build.yml +++ b/.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: diff --git a/coq-equations.opam b/coq-equations.opam index 97fcfbc6..7bb640ce 100644 --- a/coq-equations.opam +++ b/coq-equations.opam @@ -1,5 +1,5 @@ opam-version: "2.0" -version: "dev" +version: "8.17.dev" authors: [ "Matthieu Sozeau " "Cyprien Mangin " ] 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: [ diff --git a/src/covering.ml b/src/covering.ml index 6fcf7713..fd53df78 100644 --- a/src/covering.ml +++ b/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) = diff --git a/src/covering.mli b/src/covering.mli index e8196fb7..42d28d5c 100644 --- a/src/covering.mli +++ b/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 diff --git a/src/depelim.ml b/src/depelim.ml index 4f5cdfe0..b505a1ec 100644 --- a/src/depelim.ml +++ b/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; diff --git a/src/eqdec.ml b/src/eqdec.ml index de6ff406..a613d84b 100644 --- a/src/eqdec.ml +++ b/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 = diff --git a/src/equations.mli b/src/equations.mli index 7fbf76f2..2db7f14f 100644 --- a/src/equations.mli +++ b/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,7 +34,7 @@ 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 : @@ -42,7 +42,7 @@ val equations_interactive : 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 : diff --git a/src/equations_common.ml b/src/equations_common.ml index 5da539a0..ebf15e8e 100644 --- a/src/equations_common.ml +++ b/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,7 +54,6 @@ 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) @@ -63,7 +61,6 @@ let _ = Goptions.declare_bool_option { 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) @@ -71,7 +68,6 @@ let _ = Goptions.declare_bool_option { 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) @@ -79,7 +75,6 @@ let _ = Goptions.declare_bool_option { 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) @@ -87,7 +82,6 @@ let _ = Goptions.declare_bool_option { 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) @@ -95,7 +89,6 @@ let _ = Goptions.declare_bool_option { 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 diff --git a/src/equations_common.mli b/src/equations_common.mli index 852fdb11..fbf955bf 100644 --- a/src/equations_common.mli +++ b/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 diff --git a/src/g_equations.mlg b/src/g_equations.mlg index 690148e7..bf6d1a64 100644 --- a/src/g_equations.mlg +++ b/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: diff --git a/src/noconf.ml b/src/noconf.ml index 9ce9f2dc..c2fba27f 100644 --- a/src/noconf.ml +++ b/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 diff --git a/src/noconf_hom.ml b/src/noconf_hom.ml index eabf7e1b..fc0fbabf 100644 --- a/src/noconf_hom.ml +++ b/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 diff --git a/src/principles.ml b/src/principles.ml index 5abaaddc..f298389d 100644 --- a/src/principles.ml +++ b/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 diff --git a/src/principles_proofs.ml b/src/principles_proofs.ml index 1e5fbb41..cc2fef80 100644 --- a/src/principles_proofs.ml +++ b/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 diff --git a/src/sigma_types.ml b/src/sigma_types.ml index 4360fb25..466ec86c 100644 --- a/src/sigma_types.ml +++ b/src/sigma_types.ml @@ -121,7 +121,6 @@ let telescope env evd = function let (n, _, t) = to_tuple d in let len = succ (List.length tl) in let ts = Retyping.get_sort_of (push_rel_context tl env) !evd t in - let ts = ESorts.kind !evd ts in let ty, tys = let rec aux (ty, tyuniv, tys) ds = match ds with @@ -138,7 +137,6 @@ let telescope env evd = function let open UnivProblem in let enforce_leq env sigma t cstr = let ts = Retyping.get_sort_of env sigma t in - let ts = ESorts.kind sigma ts in UnivProblem.Set.add (ULe (ts, l)) cstr in let cstrs = enforce_leq env !evd t (UnivProblem.Set.add (ULe (tyuniv, l)) UnivProblem.Set.empty) in @@ -731,7 +729,7 @@ let smart_case (env : Environ.env) (evd : Evd.evar_map ref) (* If something is wrong here, it means that one of the parameters was * omitted or cut, which should be wrong... *) let params = List.map (Vars.lift (-(nb_cuts + oib.mind_nrealargs + 1))) params in - let goal = Termops.it_mkProd_or_LetIn goal cuts_ctx in + let goal = EConstr.it_mkProd_or_LetIn goal cuts_ctx in let goal = it_mkLambda_or_LetIn goal fresh_ctx in let params = List.map (to_constr ~abort_on_undefined_evars:false !evd) params in let goal' = to_constr ~abort_on_undefined_evars:false !evd goal in diff --git a/src/simplify.ml b/src/simplify.ml index 9b8bf13c..1bf0a061 100644 --- a/src/simplify.ml +++ b/src/simplify.ml @@ -217,7 +217,7 @@ and simplification_rule = | Infer_many and simplification_rules = (Loc.t option * simplification_rule) list -type goal = rel_context * EConstr.types * ESorts.t +type goal = rel_context * EConstr.types * Sorts.t type open_term = (goal * EConstr.existential) option * EConstr.constr exception CannotSimplify of Pp.t diff --git a/src/simplify.mli b/src/simplify.mli index b29a8ee2..cd09424b 100644 --- a/src/simplify.mli +++ b/src/simplify.mli @@ -15,7 +15,7 @@ and simplification_rule = | Infer_many and simplification_rules = (Loc.t option * simplification_rule) list -type goal = EConstr.rel_context * EConstr.types * EConstr.ESorts.t +type goal = EConstr.rel_context * EConstr.types * Sorts.t (* The [goal] corresponds to the context and type of an evar representing a * hole in the term. *) type open_term = (goal * EConstr.existential) option * EConstr.constr diff --git a/src/splitting.ml b/src/splitting.ml index e84e3286..aaf96375 100644 --- a/src/splitting.ml +++ b/src/splitting.ml @@ -176,7 +176,7 @@ let pr_program_info env sigma p = let open Pp in Names.Id.print p.program_id ++ str " : " ++ Printer.pr_econstr_env env sigma (Syntax.program_type p) ++ str " : " ++ - Printer.pr_econstr_env env sigma (mkSort (ESorts.make p.program_sort)) ++ + Printer.pr_econstr_env env sigma (mkSort p.program_sort) ++ str " ( " ++ (match p.program_rec with | Some (Structural ann) -> @@ -683,7 +683,7 @@ type program_shape = let make_program env evd p prob s rec_info = match rec_info with | Some r -> - let sort = ESorts.make p.program_sort in + let sort = p.program_sort in let lhs = id_subst r.rec_lets in (match r.rec_node with | WfRec wfr -> @@ -725,7 +725,7 @@ let make_program env evd p prob s rec_info = in Mutual (p', prob, r, s, after, (* lift 1 *)term)) | None -> - Single (p, prob, rec_info, s, fst (term_of_tree env evd (ESorts.make p.program_sort) s)) + Single (p, prob, rec_info, s, fst (term_of_tree env evd p.program_sort s)) let update_rec_info p rec_info = match p.Syntax.program_rec, rec_info.rec_node with @@ -905,7 +905,7 @@ let define_one_program_constants flags env0 isevar udecl unfold p = let evm, s' = aux env evm p.program_splitting in let isevar = ref evm in let env = Global.env () in - let term, ty = term_of_tree env isevar (ESorts.make p.program_info.program_sort) s' in + let term, ty = term_of_tree env isevar p.program_info.program_sort s' in let (cst, (evm, e)) = Equations_common.declare_constant (path_id (Id.of_string "functional" :: path)) term (Some ty) @@ -1044,7 +1044,7 @@ let solve_equations_obligations ~pm flags recids loc i sigma hook = let local_context, section_context = List.chop (List.length evcontext - section_length) evcontext in - let type_ = Termops.it_mkNamedProd_or_LetIn sigma (Evd.evar_concl evi) local_context in + let type_ = EConstr.it_mkNamedProd_or_LetIn sigma (Evd.evar_concl evi) local_context in let type_ = nf_beta env sigma type_ in env, ev, evi, local_context, type_) evars in (* Make goals from a copy of the evars *) diff --git a/src/splitting.mli b/src/splitting.mli index 2e5cca49..e4afbe04 100644 --- a/src/splitting.mli +++ b/src/splitting.mli @@ -121,7 +121,7 @@ val check_splitting : env -> Evd.evar_map -> splitting -> unit (** Compilation to Coq terms *) val term_of_tree : env -> - Evd.evar_map ref -> ESorts.t -> + Evd.evar_map ref -> Sorts.t -> splitting -> constr * constr diff --git a/src/subterm.ml b/src/subterm.ml index 8f06c3c0..49d3a2e8 100644 --- a/src/subterm.ml +++ b/src/subterm.ml @@ -46,7 +46,7 @@ let derive_subterm ~pm env sigma ~poly (ind, u as indu) = | Sorts.InSProp -> failwith "not implemented" | Sorts.InProp -> mkProp | Sorts.InSet -> mkSet - | Sorts.InType | Sorts.InQSort -> EConstr.mkSort (ESorts.make indsort) + | Sorts.InType -> EConstr.mkSort indsort in let len = List.length ctx in let params = mind.mind_nparams_rec in diff --git a/src/syntax.ml b/src/syntax.ml index 8aef4510..743e29f2 100644 --- a/src/syntax.ml +++ b/src/syntax.ml @@ -90,7 +90,7 @@ and ('a, 'b) by_annot = | WellFounded of 'b and 'a where_clause = pre_prototype * 'a list -and 'a wheres = 'a where_clause list * Vernacexpr.notation_declaration list +and 'a wheres = 'a where_clause list * Vernacexpr.decl_notation list type program = (signature * clause list) list and signature = identifier * rel_context * constr (* f : Π Δ. τ *) @@ -323,7 +323,7 @@ type program_info = { } let map_universe f u = - let u' = f (EConstr.mkSort (EConstr.ESorts.make u)) in + let u' = f (EConstr.mkSort u) in match Constr.kind (EConstr.Unsafe.to_constr u') with | Sort s -> s | _ -> assert false @@ -631,7 +631,7 @@ let is_recursive i : pre_equation wheres -> bool = fun eqs -> | _ -> false and occur_eqns eqs = List.exists occur_eqn eqs and occurs_notations nts = - List.exists (fun nt -> occur_var_constr_expr i nt.Vernacexpr.ntn_decl_interp) nts + List.exists (fun nt -> occur_var_constr_expr i nt.Vernacexpr.decl_ntn_interp) nts and occurs eqs = List.exists (fun (_,eqs) -> occur_eqns eqs) (fst eqs) || occurs_notations (snd eqs) in occurs eqs diff --git a/src/syntax.mli b/src/syntax.mli index e7b3af3e..5bf33b1d 100644 --- a/src/syntax.mli +++ b/src/syntax.mli @@ -81,7 +81,7 @@ and ('a, 'b) by_annot = | WellFounded of 'b and 'a where_clause = pre_prototype * 'a list -and 'a wheres = 'a where_clause list * Vernacexpr.notation_declaration list +and 'a wheres = 'a where_clause list * Vernacexpr.decl_notation list type program = (signature * clause list) list and signature = identifier * rel_context * constr (* f : Π Δ. τ *) and clause = Clause of Loc.t option * lhs * (clause, clause) rhs (* lhs rhs *) @@ -174,12 +174,12 @@ val pattern_of_glob_constr : Names.Id.Set.t * (user_pat, [ `any] ) DAst.t -val interp_pat : Environ.env -> Evd.evar_map -> Vernacexpr.notation_declaration list -> avoid:Id.Set.t -> +val interp_pat : Environ.env -> Evd.evar_map -> Vernacexpr.decl_notation list -> avoid:Id.Set.t -> (program_info * Names.Name.t list) option -> Constrexpr.constr_expr -> Id.Set.t * user_pats -val interp_eqn : env -> Evd.evar_map -> Vernacexpr.notation_declaration list -> program_info -> +val interp_eqn : env -> Evd.evar_map -> Vernacexpr.decl_notation list -> program_info -> avoid:Id.Set.t -> pre_equation -> pre_clause