diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-15 21:01:57 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-24 19:18:56 +0100 |
commit | a5feb9687819c5e7ef0db6e7b74d0e236a296674 (patch) | |
tree | bfd809fd50c8db88f390e3d5cba22360a0c90724 | |
parent | d437078a4ca82f7ca6d19be5ee9452359724f9a0 (diff) |
Separate checking univ_decls and obtaining universe binder names.
-rw-r--r-- | API/API.mli | 3 | ||||
-rw-r--r-- | engine/evd.ml | 2 | ||||
-rw-r--r-- | engine/evd.mli | 7 | ||||
-rw-r--r-- | engine/uState.ml | 8 | ||||
-rw-r--r-- | engine/uState.mli | 6 | ||||
-rw-r--r-- | plugins/funind/functional_principles_types.ml | 2 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 2 | ||||
-rw-r--r-- | plugins/ltac/rewrite.ml | 2 | ||||
-rw-r--r-- | plugins/setoid_ring/newring.ml | 2 | ||||
-rw-r--r-- | printing/printer.ml | 7 | ||||
-rw-r--r-- | printing/printer.mli | 1 | ||||
-rw-r--r-- | proofs/proof_global.ml | 10 | ||||
-rw-r--r-- | tactics/leminv.ml | 4 | ||||
-rw-r--r-- | vernac/class.ml | 2 | ||||
-rw-r--r-- | vernac/classes.ml | 8 | ||||
-rw-r--r-- | vernac/command.ml | 48 | ||||
-rw-r--r-- | vernac/indschemes.ml | 2 | ||||
-rw-r--r-- | vernac/lemmas.ml | 12 | ||||
-rw-r--r-- | vernac/obligations.ml | 15 | ||||
-rw-r--r-- | vernac/record.ml | 5 | ||||
-rw-r--r-- | vernac/vernacentries.ml | 6 |
21 files changed, 87 insertions, 67 deletions
diff --git a/API/API.mli b/API/API.mli index 63c675221..889050d90 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2882,7 +2882,8 @@ sig val evar_ident : evar -> evar_map -> Names.Id.t option val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list val universe_context : names:(Names.Id.t Loc.located) list -> extensible:bool -> evar_map -> - Universes.universe_binders * Univ.UContext.t + Univ.UContext.t + val universe_binders : evar_map -> Universes.universe_binders val nf_constraints : evar_map -> evar_map val from_ctx : UState.t -> evar_map diff --git a/engine/evd.ml b/engine/evd.ml index ca1196b94..67ae73ceb 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -936,6 +936,8 @@ let universe_of_name evd s = UState.universe_of_name evd.universes s let add_universe_name evd s l = { evd with universes = UState.add_universe_name evd.universes s l } +let universe_binders evd = UState.universe_binders evd.universes + let universes evd = UState.ugraph evd.universes let update_sigma_env evd env = diff --git a/engine/evd.mli b/engine/evd.mli index 36c399e98..b6157202d 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -509,7 +509,8 @@ val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map val universe_of_name : evar_map -> Id.t -> Univ.Level.t val add_universe_name : evar_map -> Id.t -> Univ.Level.t -> evar_map -val add_constraints_context : UState.t -> +val universe_binders : evar_map -> Universes.universe_binders +val add_constraints_context : UState.t -> Univ.constraints -> UState.t @@ -552,12 +553,12 @@ val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool val evar_universe_context : evar_map -> UState.t val universe_context_set : evar_map -> Univ.ContextSet.t val universe_context : names:(Id.t located) list -> extensible:bool -> evar_map -> - Universes.universe_binders * Univ.UContext.t + Univ.UContext.t val universe_subst : evar_map -> Universes.universe_opt_subst val universes : evar_map -> UGraph.t val check_univ_decl : evar_map -> UState.universe_decl -> - Universes.universe_binders * Univ.UContext.t + Univ.UContext.t val merge_universe_context : evar_map -> UState.t -> evar_map val set_universe_context : evar_map -> UState.t -> evar_map diff --git a/engine/uState.ml b/engine/uState.ml index 498d73fd3..282acb3d6 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -114,6 +114,8 @@ let of_binders b = in { ctx with uctx_names = b, rmap } +let universe_binders ctx = fst ctx.uctx_names + let instantiate_variable l b v = try v := Univ.LMap.update l (Some b) !v with Not_found -> assert false @@ -291,7 +293,7 @@ let universe_context ~names ~extensible uctx = let inst = Univ.Instance.of_array inst in let ctx = Univ.UContext.make (inst, Univ.ContextSet.constraints uctx.uctx_local) in - fst uctx.uctx_names, ctx + ctx let check_implication uctx cstrs ctx = let gr = initial_graph uctx in @@ -303,14 +305,14 @@ let check_implication uctx cstrs ctx = let check_univ_decl uctx decl = let open Misctypes in - let pl, ctx = universe_context + let ctx = universe_context ~names:decl.univdecl_instance ~extensible:decl.univdecl_extensible_instance uctx in if not decl.univdecl_extensible_constraints then check_implication uctx decl.univdecl_constraints ctx; - pl, ctx + ctx let restrict ctx vars = let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in diff --git a/engine/uState.mli b/engine/uState.mli index 7f2357a68..38af08f91 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -32,6 +32,8 @@ val of_context_set : Univ.ContextSet.t -> t val of_binders : Universes.universe_binders -> t +val universe_binders : t -> Universes.universe_binders + (** {5 Projections} *) val context_set : t -> Univ.ContextSet.t @@ -135,12 +137,12 @@ val normalize : t -> t Also return the association list of universe names and universes (including those not in [names]). *) val universe_context : names:(Id.t Loc.located) list -> extensible:bool -> t -> - Universes.universe_binders * Univ.UContext.t + Univ.UContext.t type universe_decl = (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl -val check_univ_decl : t -> universe_decl -> Universes.universe_binders * Univ.UContext.t +val check_univ_decl : t -> universe_decl -> Univ.UContext.t (** {5 TODO: Document me} *) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 996e2b6af..d5bff57af 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -348,7 +348,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) let evd',value = change_property_sort evd' s new_principle_type new_princ_name in let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let univs = (snd (Evd.universe_context ~names:[] ~extensible:true evd')) in + let univs = Evd.universe_context ~names:[] ~extensible:true evd' in let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs value in ignore( Declare.declare_constant diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 3089ec470..63896bb56 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1556,7 +1556,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in let functional_ref = - let ctx = (snd (Evd.universe_context ~names:[] ~extensible:true evm)) in + let ctx = Evd.universe_context ~names:[] ~extensible:true evm in declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res in (* Refresh the global universes, now including those of _F *) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 14b0742a7..2eb660219 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1884,7 +1884,7 @@ let declare_projection n instance_id r = in it_mkProd_or_LetIn ccl ctx in let typ = it_mkProd_or_LetIn typ ctx in - let pl, ctx = Evd.universe_context ~names:[] ~extensible:true sigma in + let ctx = Evd.universe_context ~names:[] ~extensible:true sigma in let typ = EConstr.to_constr sigma typ in let term = EConstr.to_constr sigma term in let cst = diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 1c3bdb958..a37b35b3d 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -220,7 +220,7 @@ let exec_tactic env evd n f args = let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in let nf c = nf (constr_of c) in - Array.map nf !tactic_res, snd (Evd.universe_context ~names:[] ~extensible:true evd) + Array.map nf !tactic_res, Evd.universe_context ~names:[] ~extensible:true evd let stdlib_modules = [["Coq";"Setoids";"Setoid"]; diff --git a/printing/printer.ml b/printing/printer.ml index d7bb0460d..4d5cfcba3 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -256,6 +256,13 @@ let safe_pr_constr t = let (sigma, env) = Pfedit.get_current_context () in safe_pr_constr_env env sigma t +let pr_universe_ctx_set sigma c = + if !Detyping.print_universes && not (Univ.ContextSet.is_empty c) then + fnl()++pr_in_comment (fun c -> v 0 + (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c)) c + else + mt() + let pr_universe_ctx sigma c = if !Detyping.print_universes && not (Univ.UContext.is_empty c) then fnl()++pr_in_comment (fun c -> v 0 diff --git a/printing/printer.mli b/printing/printer.mli index e014baa2c..a3d0eaac2 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -121,6 +121,7 @@ val pr_polymorphic : bool -> Pp.t val pr_cumulative : bool -> bool -> Pp.t val pr_universe_instance : evar_map -> Univ.UContext.t -> Pp.t val pr_universe_ctx : evar_map -> Univ.UContext.t -> Pp.t +val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t (** Printing global references using names as short as possible *) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index fdc9a236b..9faff3211 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -331,8 +331,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let initial_euctx = Proof.initial_euctx proof in let fpl, univs = Future.split2 fpl in let universes = if poly || now then Future.force univs else initial_euctx in - let binders, univctx = Evd.check_univ_decl (Evd.from_ctx universes) universe_decl in - let binders = if poly then Some binders else None in + let univctx = Evd.check_univ_decl (Evd.from_ctx universes) universe_decl in + let binders = if poly then Some (UState.universe_binders universes) else None in (* Because of dependent subgoals at the beginning of proofs, we could have existential variables in the initial types of goals, we need to normalise them for the kernel. *) @@ -360,7 +360,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now the body. So we keep the two sets distinct. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let ctx_body = UState.restrict ctx used_univs in - let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx_body) universe_decl in + let univs = Evd.check_univ_decl (Evd.from_ctx ctx_body) universe_decl in (initunivs, typ), ((body, Univ.ContextSet.of_context univs), eff) else (* Since the proof is computed now, we can simply have 1 set of @@ -370,7 +370,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now TODO: check if restrict is really necessary now. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let ctx = UState.restrict universes used_univs in - let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in + let univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in (univs, typ), ((body, Univ.ContextSet.empty), eff) in fun t p -> Future.split2 (Future.chain p (make_body t)) @@ -383,7 +383,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now the declaration as well. If the declaration is non-extensible, this will prevent the body from adding universes and constraints. *) let bodyunivs = constrain_variables univctx (Future.force univs) in - let _, univs = Evd.check_univ_decl (Evd.from_ctx bodyunivs) universe_decl in + let univs = Evd.check_univ_decl (Evd.from_ctx bodyunivs) universe_decl in (pt,Univ.ContextSet.of_context univs),eff) in let entry_fn p (_, t) = diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 62f3866de..4d1b271d6 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -235,9 +235,9 @@ let inversion_scheme env sigma t sort dep_option inv_op = p, Evd.universe_context ~names:[] ~extensible:true sigma let add_inversion_lemma name env sigma t sort dep inv_op = - let invProof, ctx = inversion_scheme env sigma t sort dep inv_op in + let invProof, univs = inversion_scheme env sigma t sort dep inv_op in let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ()) - ~univs:(snd ctx) invProof in + ~univs invProof in let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in () diff --git a/vernac/class.ml b/vernac/class.ml index 44f20a088..e59482b71 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -212,7 +212,7 @@ let build_id_coercion idf_opt source poly = Id.of_string ("Id_"^(ident_key_of_class source)^"_"^ (ident_key_of_class cl)) in - let univs = (snd (Evd.universe_context ~names:[] ~extensible:true sigma)) in + let univs = Evd.universe_context ~names:[] ~extensible:true sigma in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry (definition_entry ~types:typ_f ~poly ~univs diff --git a/vernac/classes.ml b/vernac/classes.ml index ed37bab6d..6f5f96ee2 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -119,14 +119,14 @@ let declare_instance_constant k info global imps ?hook id decl poly evm term ter (Univops.universes_of_constr term) in Evd.restrict_universe_context evm levels in - let pl, uctx = Evd.check_univ_decl evm decl in + let uctx = Evd.check_univ_decl evm decl in let entry = Declare.definition_entry ~types:termtype ~poly ~univs:uctx term in let cdecl = (DefinitionEntry entry, kind) in let kn = Declare.declare_constant id cdecl in Declare.definition_message id; - Universes.register_universe_binders (ConstRef kn) pl; + Universes.register_universe_binders (ConstRef kn) (Evd.universe_binders evm); instance_hook k info global imps ?hook (ConstRef kn); id @@ -203,12 +203,12 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) nf t in Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype); - let pl, ctx = Evd.check_univ_decl !evars decl in + let ctx = Evd.check_univ_decl !evars decl in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id (ParameterEntry (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in - Universes.register_universe_binders (ConstRef cst) pl; + Universes.register_universe_binders (ConstRef cst) (Evd.universe_binders !evars); instance_hook k pri global imps ?hook (ConstRef cst); id end else ( diff --git a/vernac/command.ml b/vernac/command.ml index 5d83de070..5a063f173 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -107,8 +107,9 @@ let interp_definition pl bl p red_option c ctypopt = let body = nf (it_mkLambda_or_LetIn c ctx) in let vars = Univops.universes_of_constr body in let evd = Evd.restrict_universe_context !evdref vars in - let pl, uctx = Evd.check_univ_decl evd decl in - imps1@(Impargs.lift_implicits nb_args imps2), pl, + let uctx = Evd.check_univ_decl evd decl in + let binders = Evd.universe_binders evd in + imps1@(Impargs.lift_implicits nb_args imps2), binders, definition_entry ~univs:uctx ~poly:p body | Some ctyp -> let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in @@ -133,8 +134,9 @@ let interp_definition pl bl p red_option c ctypopt = let vars = Univ.LSet.union (Univops.universes_of_constr body) (Univops.universes_of_constr typ) in let ctx = Evd.restrict_universe_context !evdref vars in - let pl, uctx = Evd.check_univ_decl ctx decl in - imps1@(Impargs.lift_implicits nb_args impsty), pl, + let uctx = Evd.check_univ_decl ctx decl in + let binders = Evd.universe_binders evd in + imps1@(Impargs.lift_implicits nb_args impsty), binders, definition_entry ~types:typ ~poly:p ~univs:uctx body in @@ -277,9 +279,10 @@ let do_assumptions_bound_univs coe kind nl id pl c = let ty = nf ty in let vars = Univops.universes_of_constr ty in let evd = Evd.restrict_universe_context !evdref vars in - let pl, uctx = Evd.check_univ_decl evd decl in + let uctx = Evd.check_univ_decl evd decl in + let binders = Evd.universe_binders evd in let uctx = Univ.ContextSet.of_context uctx in - let (_, _, st) = declare_assumption coe kind (ty, uctx) pl impls false nl id in + let (_, _, st) = declare_assumption coe kind (ty, uctx) binders impls false nl id in st let do_assumptions kind nl l = match l with @@ -576,7 +579,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in let ctx_params = Context.Rel.map nf ctx_params in let evd = !evdref in - let pl, uctx = Evd.check_univ_decl evd decl in + let uctx = Evd.check_univ_decl evd decl in List.iter (fun c -> check_evars env_params Evd.empty evd (EConstr.of_constr c)) arities; Context.Rel.iter (fun c -> check_evars env0 Evd.empty evd (EConstr.of_constr c)) ctx_params; List.iter (fun (_,ctyps,_) -> @@ -617,7 +620,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = in (if poly && cum then Inductiveops.infer_inductive_subtyping env_ar evd mind_ent - else mind_ent), pl, impls + else mind_ent), Evd.universe_binders evd, impls (* Very syntactical equality *) let eq_local_binders bl1 bl2 = @@ -1025,17 +1028,18 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = if List.length binders_rel > 1 then let name = add_suffix recname "_func" in let hook l gr _ = - let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in - let ty = it_mkProd_or_LetIn top_arity binders_rel in - let ty = EConstr.Unsafe.to_constr ty in - let pl, univs = Evd.universe_context ~names:pl ~extensible:plext !evdref in - (*FIXME poly? *) - let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in - (** FIXME: include locality *) - let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in - let gr = ConstRef c in - if Impargs.is_implicit_args () || not (List.is_empty impls) then - Impargs.declare_manual_implicits false gr [impls] + let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in + let ty = it_mkProd_or_LetIn top_arity binders_rel in + let ty = EConstr.Unsafe.to_constr ty in + let univs = Evd.universe_context ~names:pl ~extensible:plext !evdref in + (*FIXME poly? *) + let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in + (** FIXME: include locality *) + let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in + let gr = ConstRef c in + let () = Universes.register_universe_binders gr (Evd.universe_binders !evdref) in + if Impargs.is_implicit_args () || not (List.is_empty impls) then + Impargs.declare_manual_implicits false gr [impls] in let typ = it_mkProd_or_LetIn top_arity binders in hook, name, typ @@ -1168,7 +1172,8 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in - let pl, ctx = Evd.check_univ_decl evd pl in + let ctx = Evd.check_univ_decl evd pl in + let pl = Evd.universe_binders evd in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); @@ -1200,7 +1205,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in - let pl, ctx = Evd.check_univ_decl evd pl in + let ctx = Evd.check_univ_decl evd pl in + let pl = Evd.universe_binders evd in ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index c0ddc7e2c..58f39e303 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -109,7 +109,7 @@ let _ = let define id internal ctx c t = let f = declare_constant ~internal in - let _, univs = Evd.universe_context ~names:[] ~extensible:true ctx in + let univs = Evd.universe_context ~names:[] ~extensible:true ctx in let univs = if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs else Monomorphic_const_entry univs diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index a025bfff8..cd30c7a68 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -49,7 +49,7 @@ let retrieve_first_recthm uctx = function (NamedDecl.get_value (Global.lookup_named id),variable_opacity id) | ConstRef cst -> let cb = Global.lookup_constant cst in - let (_, uctx) = UState.universe_context ~names:[] ~extensible:true uctx in + let uctx = UState.universe_context ~names:[] ~extensible:true uctx in let inst = Univ.UContext.instance uctx in let map (c, ctx) = Vars.subst_instance_constr inst c in (Option.map map (Global.body_of_constant_body cb), is_opaque cb) @@ -223,7 +223,7 @@ let compute_proof_name locality = function let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in next_global_ident_away default_thm_id avoid -let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t_i,(_,imps))) = +let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,imps))) = let t_i = norm t_i in match body with | None -> @@ -420,9 +420,9 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook = let body,opaq = retrieve_first_recthm ctx ref in let subst = Evd.evar_universe_context_subst ctx in let norm c = Universes.subst_opt_univs_constr subst c in - let binders, ctx = Evd.check_univ_decl (Evd.from_ctx ctx) decl in + let ctx = Evd.check_univ_decl (Evd.from_ctx ctx) decl in let body = Option.map norm body in - List.map_i (save_remaining_recthms kind norm ctx binders body opaq) 1 other_thms in + List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in let thms_data = (strength,ref,imps)::other_thms_data in List.iter (fun (strength,ref,imps) -> maybe_declare_manual_implicits false ref imps; @@ -513,9 +513,9 @@ let save_proof ?proof = function | _ -> None in let decl = Proof_global.get_universe_decl () in let evd = Evd.from_ctx universes in - let binders, ctx = Evd.check_univ_decl evd decl in + let ctx = Evd.check_univ_decl evd decl in let poly = pi2 k in - let binders = if poly then Some binders else None in + let binders = if poly then Some (UState.universe_binders universes) else None in Admitted(id,k,(sec_vars, poly, (typ, ctx), None), (universes, binders)) in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 590332d08..216801811 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -475,20 +475,17 @@ let declare_definition prg = (Evd.evar_universe_context_subst prg.prg_ctx) in let opaque = prg.prg_opaque in let fix_exn = Hook.get get_fix_exn () in - let pl, ctx = Evd.check_univ_decl (Evd.from_ctx prg.prg_ctx) prg.prg_univdecl in + let () = ignore(UState.check_univ_decl prg.prg_ctx prg.prg_univdecl) in let ce = definition_entry ~fix_exn ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind) ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body) in let () = progmap_remove prg in - let cst = - DeclareDef.declare_definition prg.prg_name - prg.prg_kind ce Universes.empty_binders prg.prg_implicits - (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r)) - in - Universes.register_universe_binders cst pl; - cst + let ubinders = UState.universe_binders prg.prg_ctx in + DeclareDef.declare_definition prg.prg_name + prg.prg_kind ce ubinders prg.prg_implicits + (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r)) let rec lam_index n t acc = match Constr.kind t with @@ -893,7 +890,7 @@ in let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in Univ.Instance.empty, Evd.evar_universe_context ctx' else - let (_, uctx) = UState.universe_context ~names:[] ~extensible:true ctx' in + let uctx = UState.universe_context ~names:[] ~extensible:true ctx' in Univ.UContext.instance uctx, ctx' in let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in diff --git a/vernac/record.ml b/vernac/record.ml index 6ffbd1584..9fef8f682 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -168,9 +168,10 @@ let typecheck_params_and_fields finite def id pl t ps nots fs = let typ = EConstr.to_constr evars typ in let ce t = Pretyping.check_evars env0 Evd.empty evars (EConstr.of_constr t) in let univs = Evd.check_univ_decl evars decl in + let ubinders = Evd.universe_binders evars in List.iter (iter_constr ce) (List.rev newps); List.iter (iter_constr ce) (List.rev newfs); - univs, typ, template, imps, newps, impls, newfs + ubinders, univs, typ, template, imps, newps, impls, newfs let degenerate_decl decl = let id = match RelDecl.get_name decl with @@ -605,7 +606,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then user_err Pp.(str "Priorities only allowed for type class substructures"); (* Now, younger decl in params and fields is on top *) - let (pl, ctx), arity, template, implpars, params, implfs, fields = + let pl, ctx, arity, template, implpars, params, implfs, fields = States.with_state_protection (fun () -> typecheck_params_and_fields finite (kind = Class true) idstruc pl s ps notations fs) () in let sign = structure_signature (fields@params) in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 62c7edb19..e2f28a371 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1555,8 +1555,8 @@ let vernac_check_may_eval ?loc redexp glopt rc = let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in Evarconv.check_problems_are_solved env sigma'; let sigma',nf = Evarutil.nf_evars_and_universes sigma' in - let pl, uctx = Evd.universe_context ~names:[] ~extensible:true sigma' in - let env = Environ.push_context uctx (Evarutil.nf_env_evar sigma' env) in + let uctx = Evd.universe_context_set sigma' in + let env = Environ.push_context_set uctx (Evarutil.nf_env_evar sigma' env) in let c = nf c in let j = if Evarutil.has_undefined_evars sigma' (EConstr.of_constr c) then @@ -1572,7 +1572,7 @@ let vernac_check_may_eval ?loc redexp glopt rc = let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in Feedback.msg_notice (print_judgment env sigma' j ++ pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++ - Printer.pr_universe_ctx sigma uctx) + Printer.pr_universe_ctx_set sigma uctx) | Some r -> let (sigma',r_interp) = Hook.get f_interp_redexp env sigma' r in let redfun env evm c = |