From 84c46e5dbf55670b2e4167bf21231537b00cc4fb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 22 Sep 2023 15:10:30 +0200 Subject: [PATCH] Adapt to coq/coq#17836 (sort poly) --- .../src/g_metacoq_safechecker.mlg | 11 +++-- template-coq/src/ast_denoter.ml | 6 +-- template-coq/src/ast_quoter.ml | 40 ++++++++++++------- template-coq/src/constr_denoter.ml | 4 +- template-coq/src/constr_quoter.ml | 39 +++++++++++------- template-coq/src/denoter.ml | 12 ++++-- template-coq/src/plugin_core.ml | 4 +- template-coq/src/quoter.ml | 18 ++++----- template-coq/src/run_template_monad.ml | 27 +++++++------ template-coq/src/template_monad.ml | 3 +- template-coq/src/template_monad.mli | 2 +- template-coq/src/tm_util.ml | 10 +++-- 12 files changed, 102 insertions(+), 74 deletions(-) diff --git a/safechecker-plugin/src/g_metacoq_safechecker.mlg b/safechecker-plugin/src/g_metacoq_safechecker.mlg index e47330a8a..dce08991b 100644 --- a/safechecker-plugin/src/g_metacoq_safechecker.mlg +++ b/safechecker-plugin/src/g_metacoq_safechecker.mlg @@ -23,7 +23,7 @@ let check env evm poly (c, ustate) = let uctx = if poly then let uctx = Evd.to_universe_context evm in - let inst, auctx = Univ.abstract_universes uctx in + let inst, auctx = UVars.abstract_universes uctx in Ast_quoter.mkPolymorphic_ctx (Ast_quoter.quote_abstract_univ_context auctx) else Ast_quoter.mkMonomorphic_ctx () in @@ -55,15 +55,18 @@ let retypecheck_term_dependencies env gr = let typecheck env c = ignore (Typeops.infer env c) in let typecheck_constant c = let auctx = Environ.constant_context env c in - let names = Univ.AbstractContext.names auctx in + let qnames, unames as names = UVars.AbstractContext.names auctx in let dp = Names.DirPath.make [Names.Id.of_string "MetaCoq"; Names.Id.of_string "Retypecheck"] in + let fake_quality i _ = + Sorts.Quality.QVar (Sorts.QVar.make_unif "" i) + in let fake_level i _ = Univ.Level.make (Univ.UGlobal.make dp "" i) in - let fake_inst = Univ.Instance.of_array (Array.mapi fake_level names) in + let fake_inst = UVars.Instance.of_array (Array.mapi fake_quality qnames, Array.mapi fake_level unames) in let cu = (c, fake_inst) in let cbody, ctype, cstrs = Environ.constant_value_and_type env cu in - let env' = Environ.push_context (Univ.UContext.make names (fake_inst, cstrs)) env in + let env' = Environ.push_context (UVars.UContext.make names (fake_inst, cstrs)) env in typecheck env' ctype; Option.iter (typecheck env') cbody in diff --git a/template-coq/src/ast_denoter.ml b/template-coq/src/ast_denoter.ml index 25a4ac612..64184b91d 100644 --- a/template-coq/src/ast_denoter.ml +++ b/template-coq/src/ast_denoter.ml @@ -188,7 +188,7 @@ struct let { inductive_mind = kn; inductive_ind = i } = q in (MutInd.make1 (unquote_kn kn), unquote_int i) - (*val unquote_univ_instance : quoted_univ_instance -> Univ.Instance.t *) + (*val unquote_univ_instance : quoted_univ_instance -> UVars.Instance.t *) let unquote_proj (q : quoted_proj) : (quoted_inductive * quoted_int * quoted_int) = let { proj_ind = ind; proj_npars = ps; proj_arg = idx } = q in (ind, ps, idx) @@ -223,8 +223,8 @@ struct let u = List.fold_left Univ.Universe.sup (List.hd l) (List.tl l) in evd, Sorts.sort_of_univ u - let unquote_universe_instance(evm: Evd.evar_map) (l: quoted_univ_instance): Evd.evar_map * Univ.Instance.t - = (evm, Univ.Instance.of_array (Array.of_list (List0.map unquote_level l))) + let unquote_universe_instance(evm: Evd.evar_map) (l: quoted_univ_instance): Evd.evar_map * UVars.Instance.t + = (evm, UVars.Instance.of_array ([||], Array.of_list (List0.map unquote_level l))) let unquote_global_reference (trm : Kernames.global_reference) : GlobRef.t = diff --git a/template-coq/src/ast_quoter.ml b/template-coq/src/ast_quoter.ml index 6c209d0d5..f29962f7f 100644 --- a/template-coq/src/ast_quoter.ml +++ b/template-coq/src/ast_quoter.ml @@ -156,10 +156,13 @@ struct try ((quote_nonprop_level l, quote_constraint_type ct), quote_nonprop_level l') with e -> assert false - let quote_univ_instance (i : Univ.Instance.t) : quoted_univ_instance = - let arr = Univ.Instance.to_array i in + let quote_univ_instance (i : UVars.Instance.t) : quoted_univ_instance = + let qarr, uarr = UVars.Instance.to_array i in + let () = if not (CArray.is_empty qarr) then + CErrors.user_err Pp.(str "Quoting sort polymorphic instances not yet supported.") + in (* we assume that valid instances do not contain [Prop] or [SProp] *) - try CArray.map_to_list quote_nonprop_level arr + try CArray.map_to_list quote_nonprop_level uarr with e -> assert false (* (Prop, Le | Lt, l), (Prop, Eq, Prop) -- trivial, (l, c, Prop) -- unsatisfiable *) @@ -173,16 +176,20 @@ struct let l = constraints_ (Univ.Constraints.elements c) in Universes0.ConstraintSet.(List.fold_right add l empty) - let quote_variance (v : Univ.Variance.t) = + let quote_variance (v : UVars.Variance.t) = match v with - | Univ.Variance.Irrelevant -> Universes0.Variance.Irrelevant - | Univ.Variance.Covariant -> Universes0.Variance.Covariant - | Univ.Variance.Invariant -> Universes0.Variance.Invariant - - let quote_univ_context (uctx : Univ.UContext.t) : quoted_univ_context = - let names = CArray.map_to_list quote_name (Univ.UContext.names uctx) in - let levels = Univ.UContext.instance uctx in - let constraints = Univ.UContext.constraints uctx in + | Irrelevant -> Universes0.Variance.Irrelevant + | Covariant -> Universes0.Variance.Covariant + | Invariant -> Universes0.Variance.Invariant + + let quote_univ_context (uctx : UVars.UContext.t) : quoted_univ_context = + let qarr, uarr = (UVars.UContext.names uctx) in + let () = if not (CArray.is_empty qarr) then + CErrors.user_err Pp.(str "Quoting sort polymorphic ucontext not yet supported.") + in + let names = CArray.map_to_list quote_name uarr in + let levels = UVars.UContext.instance uctx in + let constraints = UVars.UContext.constraints uctx in (names, (quote_univ_instance levels, quote_univ_constraints constraints)) let quote_univ_contextset (uctx : Univ.ContextSet.t) : quoted_univ_contextset = @@ -196,9 +203,12 @@ struct (Universes0.LevelSetProp.of_list levels, quote_univ_constraints constraints) let quote_abstract_univ_context uctx : quoted_abstract_univ_context = - let names = Univ.AbstractContext.names uctx in - let levels = CArray.map_to_list quote_name names in - let constraints = Univ.UContext.constraints (Univ.AbstractContext.repr uctx) in + let qnames, unames = UVars.AbstractContext.names uctx in + let () = if not (CArray.is_empty qnames) then + CErrors.user_err Pp.(str "Quoting sort polymorphic abstract universe context not yet supported.") + in + let levels = CArray.map_to_list quote_name unames in + let constraints = UVars.UContext.constraints (UVars.AbstractContext.repr uctx) in (levels, quote_univ_constraints constraints) let quote_context_decl na b t = diff --git a/template-coq/src/constr_denoter.ml b/template-coq/src/constr_denoter.ml index f4ea317e5..06c40fb90 100644 --- a/template-coq/src/constr_denoter.ml +++ b/template-coq/src/constr_denoter.ml @@ -264,10 +264,10 @@ struct let unquote_universe_instance evm trm (* of type universe_instance *) = let l = unquote_list trm in let evm, l = map_evm unquote_level evm l in - evm, Univ.Instance.of_array (Array.of_list l) + evm, UVars.Instance.of_array ([||], Array.of_list l) let unquote_variance v = - let open Univ.Variance in + let open UVars.Variance in if constr_equall v cIrrelevant then Irrelevant else if constr_equall v cCovariant then Covariant else if constr_equall v cInvariant then Invariant diff --git a/template-coq/src/constr_quoter.ml b/template-coq/src/constr_quoter.ml index 671c94dc6..c63bd9968 100644 --- a/template-coq/src/constr_quoter.ml +++ b/template-coq/src/constr_quoter.ml @@ -229,9 +229,12 @@ struct (* todo : can be deduced from quote_level, hence shoud be in the Reify module *) let quote_univ_instance u = - let arr = Univ.Instance.to_array u in + let qarr, uarr = UVars.Instance.to_array u in + let () = if not (CArray.is_empty qarr) then + CErrors.user_err Pp.(str "Quoting sort polymorphic instances not yet supported.") + in (* we assume that valid instances do not contain [Prop] or [SProp] *) - to_coq_listl tlevel (CArray.map_to_list quote_nonprop_level arr) + to_coq_listl tlevel (CArray.map_to_list quote_nonprop_level uarr) let is_Lt = function | Univ.Lt -> true @@ -260,9 +263,9 @@ struct let quote_variance v = match v with - | Univ.Variance.Irrelevant -> Lazy.force cIrrelevant - | Univ.Variance.Covariant -> Lazy.force cCovariant - | Univ.Variance.Invariant -> Lazy.force cInvariant + | UVars.Variance.Irrelevant -> Lazy.force cIrrelevant + | UVars.Variance.Covariant -> Lazy.force cCovariant + | UVars.Variance.Invariant -> Lazy.force cInvariant let quote_cuminfo_variance var = let var_list = CArray.map_to_list quote_variance var in @@ -274,10 +277,13 @@ struct pairl tLevelSet tConstraintSet levels' const' let quote_univ_context uctx = - let arr = (UContext.names uctx) in - let idents = to_coq_listl tname (CArray.map_to_list quote_name arr) in - let inst' = quote_univ_instance (UContext.instance uctx) in - let const' = quote_univ_constraints (UContext.constraints uctx) in + let qarr, uarr = (UVars.UContext.names uctx) in + let () = if not (CArray.is_empty qarr) then + CErrors.user_err Pp.(str "Quoting sort polymorphic ucontext not yet supported.") + in + let idents = to_coq_listl tname (CArray.map_to_list quote_name uarr) in + let inst' = quote_univ_instance (UVars.UContext.instance uctx) in + let const' = quote_univ_constraints (UVars.UContext.constraints uctx) in let p = constr_mkApp (tUContextmake', [|inst'; const'|]) in constr_mkApp (tUContextmake, [|idents; p |]) @@ -290,9 +296,12 @@ struct constr_mkApp (cSome, [| listvar; var' |]) *) let quote_abstract_univ_context uctx = - let arr = (AbstractContext.names uctx) in - let idents = to_coq_listl tname (CArray.map_to_list quote_name arr) in - let const' = quote_univ_constraints (UContext.constraints (AbstractContext.repr uctx)) in + let qarr, uarr = (UVars.AbstractContext.names uctx) in + let () = if not (CArray.is_empty qarr) then + CErrors.user_err Pp.(str "Quoting sort polymorphic abstract universe context not yet supported.") + in + let idents = to_coq_listl tname (CArray.map_to_list quote_name uarr) in + let const' = quote_univ_constraints (UVars.UContext.constraints (UVars.AbstractContext.repr uctx)) in constr_mkApp (tAUContextmake, [|idents; const'|]) let mkMonomorphic_ctx () = Lazy.force cMonomorphic_ctx @@ -309,15 +318,15 @@ struct let quote_inductive_universes uctx = match uctx with | Entries.Monomorphic_entry -> - let f inst = Array.map (fun _ -> Anonymous) (Instance.to_array inst) in - let ctx = quote_univ_context (Univ.ContextSet.to_context f Univ.ContextSet.empty) in + let f inst = assert (UVars.Instance.is_empty inst); [||], [||] in + let ctx = quote_univ_context (UVars.UContext.of_context_set f Sorts.QVar.Set.empty Univ.ContextSet.empty) in constr_mkApp (cMonomorphic_entry, [| ctx |]) | Entries.Polymorphic_entry uctx -> let ctx = quote_univ_context uctx in constr_mkApp (cPolymorphic_entry, [| ctx |]) let quote_ugraph (g : UGraph.t) = - let inst' = quote_univ_instance Univ.Instance.empty in + let inst' = quote_univ_instance UVars.Instance.empty in let const' = quote_univ_constraints (fst (UGraph.constraints_of_universes g)) in let uctx = constr_mkApp (tUContextmake, [|inst' ; const'|]) in constr_mkApp (tadd_global_constraints, [|constr_mkApp (cMonomorphic_ctx, [| uctx |]); Lazy.force tinit_graph|]) diff --git a/template-coq/src/denoter.ml b/template-coq/src/denoter.ml index b6bb08ccc..221dd8bac 100644 --- a/template-coq/src/denoter.ml +++ b/template-coq/src/denoter.ml @@ -20,10 +20,10 @@ sig val unquote_cast_kind : quoted_cast_kind -> Constr.cast_kind val unquote_kn : quoted_kernel_name -> KerName.t val unquote_inductive : quoted_inductive -> Names.inductive - (*val unquote_univ_instance : quoted_univ_instance -> Univ.Instance.t *) + (*val unquote_univ_instance : quoted_univ_instance -> UVars.Instance.t *) val unquote_proj : quoted_proj -> (quoted_inductive * quoted_int * quoted_int) val unquote_universe : Evd.evar_map -> quoted_sort -> Evd.evar_map * Sorts.t - val unquote_universe_instance: Evd.evar_map -> quoted_univ_instance -> Evd.evar_map * Univ.Instance.t + val unquote_universe_instance: Evd.evar_map -> quoted_univ_instance -> Evd.evar_map * UVars.Instance.t (* val representsIndConstuctor : quoted_inductive -> Term.constr -> bool *) val inspect_term : t -> (t, quoted_int, quoted_ident, quoted_aname, quoted_sort, quoted_cast_kind, quoted_kernel_name, quoted_inductive, quoted_relevance, quoted_univ_instance, quoted_proj, @@ -154,10 +154,14 @@ struct let ind' = D.unquote_inductive ind in let proj_arg = D.unquote_int arg in let mib = Environ.lookup_mind (fst ind') env in - let p' = Declareops.inductive_make_projection ind' mib ~proj_arg in + let p', r = Declareops.inductive_make_projection ind' mib ~proj_arg in let p' = Names.Projection.make p' false in let evm, t' = aux env evm t in - evm, Constr.mkProj (p', t') + let r = match r with + | Relevant | Irrelevant -> r + | RelevanceVar _ -> CErrors.user_err Pp.(str "Unquoting sort poly projections not yet supported.") + in + evm, Constr.mkProj (p', r, t') | ACoq_tInt x -> evm, Constr.mkInt (D.unquote_int63 x) | ACoq_tFloat x -> evm, Constr.mkFloat (D.unquote_float64 x) diff --git a/template-coq/src/plugin_core.ml b/template-coq/src/plugin_core.ml index d487dab5d..6f26784ef 100644 --- a/template-coq/src/plugin_core.ml +++ b/template-coq/src/plugin_core.ml @@ -281,10 +281,10 @@ let tmInductive (infer_univs : bool) (mie : mutual_inductive_entry) : unit tm = if infer_univs then let evm = Evd.from_env env in let ctx, mie = Tm_util.RetypeMindEntry.infer_mentry_univs env evm mie in - DeclareUctx.declare_universe_context ~poly:false ctx; mie + Global.push_context_set ~strict:true ctx; mie else mie in - let names = (UState.Monomorphic_entry Univ.ContextSet.empty, Names.Id.Map.empty) in + let names = (UState.Monomorphic_entry Univ.ContextSet.empty, UnivNames.empty_binders) in ignore (DeclareInd.declare_mutual_inductive_with_eliminations mie names []) ; success ~st (Global.env ()) evd () diff --git a/template-coq/src/quoter.ml b/template-coq/src/quoter.ml index 2bcb1780b..8889077f9 100644 --- a/template-coq/src/quoter.ml +++ b/template-coq/src/quoter.ml @@ -105,12 +105,12 @@ sig val quote_constraint_type : Univ.constraint_type -> quoted_constraint_type val quote_univ_constraint : Univ.univ_constraint -> quoted_univ_constraint - val quote_univ_instance : Univ.Instance.t -> quoted_univ_instance + val quote_univ_instance : UVars.Instance.t -> quoted_univ_instance val quote_univ_constraints : Univ.Constraints.t -> quoted_univ_constraints - val quote_univ_context : Univ.UContext.t -> quoted_univ_context + val quote_univ_context : UVars.UContext.t -> quoted_univ_context val quote_univ_contextset : Univ.ContextSet.t -> quoted_univ_contextset - val quote_variance : Univ.Variance.t -> quoted_variance - val quote_abstract_univ_context : Univ.AbstractContext.t -> quoted_abstract_univ_context + val quote_variance : UVars.Variance.t -> quoted_variance + val quote_abstract_univ_context : UVars.AbstractContext.t -> quoted_abstract_univ_context val mkMonomorphic_entry : quoted_univ_contextset -> quoted_universes_entry val mkPolymorphic_entry : quoted_univ_context -> quoted_universes_entry @@ -185,8 +185,8 @@ struct let get_abstract_inductive_universes iu = match iu with - | Declarations.Monomorphic -> Univ.UContext.empty - | Polymorphic ctx -> Univ.AbstractContext.repr ctx + | Declarations.Monomorphic -> UVars.UContext.empty + | Polymorphic ctx -> UVars.AbstractContext.repr ctx let quote_universes_entry = function | Monomorphic_entry -> Q.mkMonomorphic_entry (Q.quote_univ_contextset Univ.ContextSet.empty) @@ -336,7 +336,7 @@ struct | Constr.Fix fp -> quote_fixpoint acc env sigma fp | Constr.CoFix fp -> quote_cofixpoint acc env sigma fp - | Constr.Proj (p,c) -> + | Constr.Proj (p,_,c) -> let ind = quote_inductive' (Projection.inductive p) in let pars = Q.quote_int (Projection.npars p) in let arg = Q.quote_int (Projection.arg p) in @@ -368,7 +368,7 @@ struct (Q.mkCoFix (a',decl'), acc) and quote_minductive_type (acc : 'a) env sigma (t : MutInd.t) mib = let uctx = get_abstract_inductive_universes mib.Declarations.mind_universes in - let inst = Univ.UContext.instance uctx in + let inst = UVars.UContext.instance uctx in let indtys = (CArray.map_to_list (fun oib -> let ty = Inductive.type_of_inductive ((mib,oib),inst) in @@ -649,7 +649,7 @@ since [absrt_info] is a private type *) let quote_constant_entry bypass env evm cd = let (ty, body) = quote_constant_body_aux bypass env evm cd in let uctx = match cd.const_universes with - | Polymorphic auctx -> Polymorphic_entry (Univ.AbstractContext.repr auctx) + | Polymorphic auctx -> Polymorphic_entry (UVars.AbstractContext.repr auctx) | Monomorphic -> Monomorphic_entry in let univs = quote_universes_entry uctx in diff --git a/template-coq/src/run_template_monad.ml b/template-coq/src/run_template_monad.ml index 681adb262..056ceba8d 100644 --- a/template-coq/src/run_template_monad.ml +++ b/template-coq/src/run_template_monad.ml @@ -1,4 +1,5 @@ open Univ +open UVars open Entries open Names open Redops @@ -152,23 +153,23 @@ let denote_names evm trm : _ * Name.t array = let l = unquote_list trm in evm, CArray.map_of_list unquote_name l -let denote_ucontext env evm trm (* of type UContext.t *) : _ * UContext.t = +let denote_ucontext env evm trm (* of type UContext.t *) : _ * UVars.UContext.t = let l, c = unquote_pair trm in let evm, names = denote_names evm l in let l, c = unquote_pair c in let l = unquote_list l in let evm, vars = map_evm unquote_level evm l in let evm, c = unquote_constraints env evm c in - let inst = Instance.of_array (Array.of_list vars) in - evm, (UContext.make names (inst, c)) + let inst = Instance.of_array ([||], Array.of_list vars) in + evm, (UVars.UContext.make ([||], names) (inst, c)) -let denote_aucontext env evm trm (* of type AbstractContext.t *) : _ * AbstractContext.t = +let denote_aucontext env evm trm (* of type AbstractContext.t *) : _ * UVars.AbstractContext.t = let i, c = unquote_pair trm in let l = unquote_list i in let vars = List.mapi (fun i l -> Level.var i) l in - let vars = Instance.of_array (Array.of_list vars) in + let vars = Instance.of_array ([||], Array.of_list vars) in let evm, c = unquote_constraints env evm c in - evm, snd (abstract_universes (UContext.make (CArray.map_of_list unquote_name l) (vars, c))) + evm, snd (abstract_universes (UContext.make ([||], CArray.map_of_list unquote_name l) (vars, c))) let denote_variance trm (* of type Variance *) : Variance.t = if constr_equall trm cIrrelevant then Variance.Irrelevant @@ -189,12 +190,12 @@ let _denote_variances evm trm : _ * Variance.t array option = (* todo : stick to Coq implem *) type universe_context_type = - | Monomorphic_uctx of Univ.ContextSet.t - | Polymorphic_uctx of Univ.AbstractContext.t + | Monomorphic_uctx of ContextSet.t + | Polymorphic_uctx of AbstractContext.t let _to_entry_inductive_universes = function | Monomorphic_uctx ctx -> UState.Monomorphic_entry ctx - | Polymorphic_uctx ctx -> UState.Polymorphic_entry (Univ.AbstractContext.repr ctx) + | Polymorphic_uctx ctx -> UState.Polymorphic_entry (AbstractContext.repr ctx) let _denote_universes_decl env evm trm (* of type universes_decl *) : _ * universe_context_type = let (h, args) = app_full trm [] in @@ -300,16 +301,16 @@ let declare_inductive (env: Environ.env) (evm: Evd.evar_map) (infer_univs : bool let mind = reduce_all env evm mind in let evm' = Evd.from_env env in let evm', ctx, mind = unquote_mutual_inductive_entry env evm' mind in - let () = DeclareUctx.declare_universe_context ~poly:false ctx in + let () = Global.push_context_set ~strict:true ctx in let evm, mind = if infer_univs then let ctx, mind = Tm_util.RetypeMindEntry.infer_mentry_univs env evm' mind in debug (fun () -> Pp.(str "Declaring universe context " ++ Univ.pr_universe_context_set (Level.pr) ctx)); - DeclareUctx.declare_universe_context ~poly:false ctx; + Global.push_context_set ~strict:true ctx; Evd.merge_context_set Evd.UnivRigid evm ctx, mind else evm, mind in - let names = (UState.Monomorphic_entry Univ.ContextSet.empty, Names.Id.Map.empty) in + let names = (UState.Monomorphic_entry Univ.ContextSet.empty, UnivNames.empty_binders) in let primitive_expected = match mind.mind_entry_record with | Some (Some _) -> true @@ -322,7 +323,7 @@ let declare_inductive (env: Environ.env) (evm: Evd.evar_map) (infer_univs : bool let dflt_pf = { pf_coercion = false; pf_instance = false; pf_priority = None; pf_locality = OptDefault; pf_canonical = false; pf_reversible = false} in let decl_projs i oie = let ind = (ind_kn, i) in - let univs = (Entries.Monomorphic_entry, Names.Id.Map.empty) in + let univs = (Entries.Monomorphic_entry, UnivNames.empty_binders) in let inhabitant_id = List.hd oie.mind_entry_consnames in let fields, _ = Term.decompose_prod_assum (List.hd oie.mind_entry_lc) in let fieldimpls = List.map (fun _ -> []) fields in diff --git a/template-coq/src/template_monad.ml b/template-coq/src/template_monad.ml index da3592251..fa5aa34b5 100644 --- a/template-coq/src/template_monad.ml +++ b/template-coq/src/template_monad.ml @@ -1,4 +1,3 @@ -open Univ open Names open GlobRef open Pp @@ -228,7 +227,7 @@ let next_action env evd (pgm : constr) : template_monad * _ = | Const (c, u) -> ConstRef c, u | Ind (i, u) -> IndRef i, u | Construct (c, u) -> ConstructRef c, u - | Var id -> VarRef id, Instance.empty + | Var id -> VarRef id, UVars.Instance.empty | _ -> raise Not_found with _ -> CErrors.user_err (str "Invalid argument or not yet implemented. The argument must be a TemplateProgram: " ++ Printer.pr_constr_env env evd coConstr) diff --git a/template-coq/src/template_monad.mli b/template-coq/src/template_monad.mli index ac2cce6c7..50fc73b94 100644 --- a/template-coq/src/template_monad.mli +++ b/template-coq/src/template_monad.mli @@ -62,4 +62,4 @@ val app_full val next_action - : Environ.env -> Evd.evar_map -> Constr.t -> (template_monad * Univ.Instance.t) + : Environ.env -> Evd.evar_map -> Constr.t -> (template_monad * UVars.Instance.t) diff --git a/template-coq/src/tm_util.ml b/template-coq/src/tm_util.ml index fb60bd985..8667157b3 100644 --- a/template-coq/src/tm_util.ml +++ b/template-coq/src/tm_util.ml @@ -139,7 +139,6 @@ module CaseCompat = open Context.Rel.Declaration open Vars open Util - open Univ open Declarations (** {6 Changes of representation of Case nodes} *) @@ -170,7 +169,7 @@ module CaseCompat = let realdecls, _ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in let self = let args = Context.Rel.instance mkRel 0 mip.mind_arity_ctxt in - let inst = Instance.of_array (Array.init (Instance.length u) Level.var) in + let inst = UVars.Instance.abstract_instance (UVars.Instance.length u) in mkApp (mkIndU (ci.ci_ind, inst), args) in let realdecls = LocalAssum (Context.anonR, self) :: realdecls in @@ -298,8 +297,11 @@ module RetypeMindEntry = | Entries.Monomorphic_ind_entry -> evm | Entries.Template_ind_entry uctx -> evm | Entries.Polymorphic_ind_entry uctx -> - let uctx' = ContextSet.of_context uctx in - Evd.merge_context_set (UState.UnivFlexible false) evm uctx' + let qs, (us, csts) = UVars.UContext.to_context_set uctx in + let qs = Sorts.Quality.Set.fold (fun q qs -> match q with + | QConstant _ -> assert false + | QVar q -> Sorts.QVar.Set.add q qs) qs Sorts.QVar.Set.empty in + Evd.merge_sort_context_set (UState.UnivFlexible false) evm ((qs,us),csts) in let evm, mind = infer_mentry_univs env evm mind in let evm = Evd.minimize_universes evm in