aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/class.ml4
-rw-r--r--vernac/classes.ml46
-rw-r--r--vernac/command.ml255
-rw-r--r--vernac/command.mli4
-rw-r--r--vernac/declareDef.ml7
-rw-r--r--vernac/declareDef.mli7
-rw-r--r--vernac/indschemes.ml6
-rw-r--r--vernac/lemmas.ml65
-rw-r--r--vernac/lemmas.mli2
-rw-r--r--vernac/locality.ml57
-rw-r--r--vernac/locality.mli13
-rw-r--r--vernac/obligations.ml168
-rw-r--r--vernac/obligations.mli2
-rw-r--r--vernac/record.ml125
-rw-r--r--vernac/record.mli24
-rw-r--r--vernac/vernacentries.ml403
-rw-r--r--vernac/vernacentries.mli2
-rw-r--r--vernac/vernacinterp.ml15
-rw-r--r--vernac/vernacinterp.mli16
-rw-r--r--vernac/vernacstate.ml30
-rw-r--r--vernac/vernacstate.mli2
21 files changed, 650 insertions, 603 deletions
diff --git a/vernac/class.ml b/vernac/class.ml
index 44f20a0887..943da8fa8a 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -212,10 +212,10 @@ 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.const_univ_entry ~poly sigma in
let constr_entry = (* Cast is necessary to express [val_f] is identity *)
DefinitionEntry
- (definition_entry ~types:typ_f ~poly ~univs
+ (definition_entry ~types:typ_f ~univs
~inline:true (mkCast (val_f, DEFAULTcast, typ_f)))
in
let decl = (constr_entry, IsDefinition IdentityCoercion) in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 20cb43b24e..cb1d2f7c73 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 ~poly evm decl in
let entry =
- Declare.definition_entry ~types:termtype ~poly ~univs:uctx term
+ Declare.definition_entry ~types:termtype ~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;
+ Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders evm);
instance_hook k info global imps ?hook (ConstRef kn);
id
@@ -200,16 +200,16 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
let nf, subst = Evarutil.e_nf_evars_and_universes evars in
let termtype =
let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
- 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 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;
- instance_hook k pri global imps ?hook (ConstRef cst); id
+ nf t
+ in
+ Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype);
+ let univs = Evd.check_univ_decl ~poly !evars decl in
+ let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
+ (ParameterEntry
+ (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
+ in
+ Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders !evars);
+ instance_hook k pri global imps ?hook (ConstRef cst); id
end
else (
let props =
@@ -384,14 +384,17 @@ let context poly l =
let uctx = ref (Evd.universe_context_set !evars) in
let fn status (id, b, t) =
if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
- let ctx = Univ.ContextSet.to_context !uctx in
(* Declare the universe context once *)
+ let univs = if poly
+ then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx)
+ else Monomorphic_const_entry !uctx
+ in
let () = uctx := Univ.ContextSet.empty in
let decl = match b with
| None ->
- (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical)
+ (ParameterEntry (None,(t,univs),None), IsAssumption Logical)
| Some b ->
- let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in
+ let entry = Declare.definition_entry ~univs ~types:t b in
(DefinitionEntry entry, IsAssumption Logical)
in
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
@@ -409,16 +412,19 @@ let context poly l =
in
let impl = List.exists test impls in
let decl = (Discharge, poly, Definitional) in
+ let univs = if poly
+ then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx)
+ else Monomorphic_const_entry !uctx
+ in
let nstatus = match b with
| None ->
- pi3 (Command.declare_assumption false decl (t, !uctx) [] [] impl
+ pi3 (Command.declare_assumption false decl (t, univs) Universes.empty_binders [] impl
Vernacexpr.NoInline (Loc.tag id))
| Some b ->
- let ctx = Univ.ContextSet.to_context !uctx in
let decl = (Discharge, poly, Definition) in
- let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in
+ let entry = Declare.definition_entry ~univs ~types:t b in
let hook = Lemmas.mk_hook (fun _ gr -> gr) in
- let _ = DeclareDef.declare_definition id decl entry [] [] hook in
+ let _ = DeclareDef.declare_definition id decl entry Universes.empty_binders [] hook in
Lib.sections_are_opened () || Lib.is_modtype_strict ()
in
status && nstatus
diff --git a/vernac/command.ml b/vernac/command.ml
index 257c003b5a..66d4fe9847 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -88,14 +88,14 @@ let warn_implicits_in_term =
strbrk "Implicit arguments declaration relies on type." ++ spc () ++
strbrk "The term declares more implicits than the type here.")
-let interp_definition pl bl p red_option c ctypopt =
+let interp_definition pl bl poly red_option c ctypopt =
let env = Global.env() in
let evd, decl = Univdecls.interp_univ_decl_opt env pl in
let evdref = ref evd in
let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in
let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in
let nb_args = Context.Rel.nhyps ctx in
- let imps,pl,ce =
+ let imps,ce =
match ctypopt with
None ->
let subst = evd_comb0 Evd.nf_univ_variables evdref in
@@ -105,14 +105,14 @@ let interp_definition pl bl p red_option c ctypopt =
let c = EConstr.Unsafe.to_constr c in
let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
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,
- definition_entry ~univs:uctx ~poly:p body
+ let vars = EConstr.universes_of_constr !evdref (EConstr.of_constr body) in
+ let () = evdref := Evd.restrict_universe_context !evdref vars in
+ let uctx = Evd.check_univ_decl ~poly !evdref decl in
+ imps1@(Impargs.lift_implicits nb_args imps2),
+ definition_entry ~univs:uctx body
| Some ctyp ->
- let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in
- let subst = evd_comb0 Evd.nf_univ_variables evdref in
+ let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in
+ let subst = evd_comb0 Evd.nf_univ_variables evdref in
let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
let env_bl = push_rel_context ctx env in
let c, imps2 = interp_casted_constr_evars_impls ~impls env_bl evdref c ty in
@@ -130,22 +130,22 @@ let interp_definition pl bl p red_option c ctypopt =
in
if not (try List.for_all chk imps2 with Not_found -> false)
then warn_implicits_in_term ();
- 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,
- definition_entry ~types:typ ~poly:p
- ~univs:uctx body
+ let bodyvars = EConstr.universes_of_constr !evdref (EConstr.of_constr body) in
+ let tyvars = EConstr.universes_of_constr !evdref (EConstr.of_constr ty) in
+ let vars = Univ.LSet.union bodyvars tyvars in
+ let () = evdref := Evd.restrict_universe_context !evdref vars in
+ let uctx = Evd.check_univ_decl ~poly !evdref decl in
+ imps1@(Impargs.lift_implicits nb_args impsty),
+ definition_entry ~types:typ ~univs:uctx body
in
- red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, pl, imps
+ (red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, imps)
-let check_definition (ce, evd, _, _, imps) =
+let check_definition (ce, evd, _, imps) =
check_evars_are_solved (Global.env ()) evd Evd.empty;
ce
let do_definition ident k univdecl bl red_option c ctypopt hook =
- let (ce, evd, univdecl, pl', imps as def) =
+ let (ce, evd, univdecl, imps as def) =
interp_definition univdecl bl (pi2 k) red_option c ctypopt
in
if Flags.is_program_mode () then
@@ -166,15 +166,37 @@ let do_definition ident k univdecl bl red_option c ctypopt hook =
ignore(Obligations.add_definition
ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls)
else let ce = check_definition def in
- ignore(DeclareDef.declare_definition ident k ce pl' imps
+ ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps
(Lemmas.mk_hook
(fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
(* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
+let axiom_into_instance = ref false
+
+let _ =
+ let open Goptions in
+ declare_bool_option
+ { optdepr = false;
+ optname = "automatically declare axioms whose type is a typeclass as instances";
+ optkey = ["Typeclasses";"Axioms";"Are";"Instances"];
+ optread = (fun _ -> !axiom_into_instance);
+ optwrite = (:=) axiom_into_instance; }
+
+let should_axiom_into_instance = function
+ | Discharge ->
+ (* The typeclass behaviour of Variable and Context doesn't depend
+ on section status *)
+ true
+ | Global | Local -> !axiom_into_instance
+
let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl (_,ident) =
match local with
| Discharge when Lib.sections_are_opened () ->
+ let ctx = match ctx with
+ | Monomorphic_const_entry ctx -> ctx
+ | Polymorphic_const_entry ctx -> Univ.ContextSet.of_context ctx
+ in
let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in
let _ = declare_variable ident decl in
let () = assumption_message ident in
@@ -189,24 +211,24 @@ match local with
(r,Univ.Instance.empty,true)
| Global | Local | Discharge ->
+ let do_instance = should_axiom_into_instance local in
let local = DeclareDef.get_locality ident ~kind:"axiom" local in
let inl = match nl with
| NoInline -> None
| DefaultInline -> Some (Flags.get_inline_level())
| InlineAt i -> Some i
in
- let ctx = Univ.ContextSet.to_context ctx in
- let decl = (ParameterEntry (None,p,(c,ctx),inl), IsAssumption kind) in
+ let decl = (ParameterEntry (None,(c,ctx),inl), IsAssumption kind) in
let kn = declare_constant ident ~local decl in
let gr = ConstRef kn in
let () = maybe_declare_manual_implicits false gr imps in
- let () = Universes.register_universe_binders gr pl in
+ let () = Declare.declare_univ_binders gr pl in
let () = assumption_message ident in
- let () = Typeclasses.declare_instance None false gr in
+ let () = if do_instance then Typeclasses.declare_instance None false gr in
let () = if is_coe then Class.try_add_new_coercion gr ~local p in
- let inst =
- if p (* polymorphic *) then Univ.UContext.instance ctx
- else Univ.Instance.empty
+ let inst = match ctx with
+ | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx
+ | Monomorphic_const_entry _ -> Univ.Instance.empty
in
(gr,inst,Lib.is_modtype_strict ())
@@ -216,26 +238,63 @@ let interp_assumption evdref env impls bl c =
let ty = EConstr.Unsafe.to_constr ty in
(ty, impls)
-let declare_assumptions idl is_coe k (c,ctx) pl imps impl_is_on nl =
+(* When monomorphic the universe constraints are declared with the first declaration only. *)
+let next_uctx =
+ let empty_uctx = Monomorphic_const_entry Univ.ContextSet.empty in
+ function
+ | Polymorphic_const_entry _ as uctx -> uctx
+ | Monomorphic_const_entry _ -> empty_uctx
+
+let declare_assumptions idl is_coe k (c,uctx) pl imps nl =
let refs, status, _ =
- List.fold_left (fun (refs,status,ctx) id ->
+ List.fold_left (fun (refs,status,uctx) id ->
let ref',u',status' =
- declare_assumption is_coe k (c,ctx) pl imps impl_is_on nl id in
- (ref',u')::refs, status' && status, Univ.ContextSet.empty)
- ([],true,ctx) idl
+ declare_assumption is_coe k (c,uctx) pl imps false nl id in
+ (ref',u')::refs, status' && status, next_uctx uctx)
+ ([],true,uctx) idl
in
List.rev refs, status
-let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
+
+let maybe_error_many_udecls = function
+ | ((loc,id), Some _) ->
+ user_err ?loc ~hdr:"many_universe_declarations"
+ Pp.(str "When declaring multiple axioms in one command, " ++
+ str "only the first is allowed a universe binder " ++
+ str "(which will be shared by the whole block).")
+ | (_, None) -> ()
+
+let process_assumptions_udecls kind l =
+ let udecl, first_id = match l with
+ | (coe, ((id, udecl)::rest, c))::rest' ->
+ List.iter maybe_error_many_udecls rest;
+ List.iter (fun (coe, (idl, c)) -> List.iter maybe_error_many_udecls idl) rest';
+ udecl, id
+ | (_, ([], _))::_ | [] -> assert false
+ in
+ let () = match kind, udecl with
+ | (Discharge, _, _), Some _ when Lib.sections_are_opened () ->
+ let loc = fst first_id in
+ let msg = Pp.str "Section variables cannot be polymorphic." in
+ user_err ?loc msg
+ | _ -> ()
+ in
+ udecl, List.map (fun (coe, (idl, c)) -> coe, (List.map fst idl, c)) l
+
+let do_assumptions kind nl l =
let open Context.Named.Declaration in
let env = Global.env () in
- let evdref = ref (Evd.from_env env) in
- let l =
- if poly then
+ let udecl, l = process_assumptions_udecls kind l in
+ let evdref, udecl =
+ let evd, udecl = Univdecls.interp_univ_decl_opt env udecl in
+ ref evd, udecl
+ in
+ let l =
+ if pi2 kind (* poly *) then
(* Separate declarations so that A B : Type puts A and B in different levels. *)
List.fold_right (fun (is_coe,(idl,c)) acc ->
- List.fold_right (fun id acc ->
- (is_coe, ([id], c)) :: acc) idl acc)
+ List.fold_right (fun id acc ->
+ (is_coe, ([id], c)) :: acc) idl acc)
l []
else l
in
@@ -247,65 +306,31 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
let ienv = List.fold_right (fun (_,id) ienv ->
let impls = compute_internalization_data env Variable t imps in
Id.Map.add id impls ienv) idl ienv in
- ((env,ienv),((is_coe,idl),t,imps)))
+ ((env,ienv),((is_coe,idl),t,imps)))
(env,empty_internalization_env) l
in
let evd = solve_remaining_evars all_and_fail_flags env !evdref Evd.empty in
(* The universe constraints come from the whole telescope. *)
let evd = Evd.nf_constraints evd in
- let ctx = Evd.universe_context_set evd in
- let nf_evar c = EConstr.Unsafe.to_constr (nf_evar evd (EConstr.of_constr c)) in
- let l = List.map (on_pi2 nf_evar) l in
- pi2 (List.fold_left (fun (subst,status,ctx) ((is_coe,idl),t,imps) ->
- let t = replace_vars subst t in
- let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) [] imps false nl in
- let subst' = List.map2
- (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u)))
- idl refs
- in
- (subst'@subst, status' && status,
- (* The universe constraints are declared with the first declaration only. *)
- Univ.ContextSet.empty)) ([],true,ctx) l)
-
-let do_assumptions_bound_univs coe kind nl id pl c =
- let env = Global.env () in
- let evd, decl = Univdecls.interp_univ_decl_opt env pl in
- let evdref = ref evd in
- let ty, impls = interp_type_evars_impls env evdref c in
- let nf, subst = Evarutil.e_nf_evars_and_universes evdref in
- let ty = EConstr.Unsafe.to_constr ty in
- 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 = Univ.ContextSet.of_context uctx in
- let (_, _, st) = declare_assumption coe kind (ty, uctx) pl impls false nl id in
- st
-
-let do_assumptions kind nl l = match l with
-| [coe, ([id, Some pl], c)] ->
- let () = match kind with
- | (Discharge, _, _) when Lib.sections_are_opened () ->
- let loc = fst id in
- let msg = Pp.str "Section variables cannot be polymorphic." in
- user_err ?loc msg
- | _ -> ()
+ let nf_evar c = EConstr.to_constr evd (EConstr.of_constr c) in
+ let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) ->
+ let t = nf_evar t in
+ let uvars = Univ.LSet.union uvars (Univops.universes_of_constr t) in
+ uvars, (coe,t,imps))
+ Univ.LSet.empty l
in
- do_assumptions_bound_univs coe kind nl id (Some pl) c
-| _ ->
- let map (coe, (idl, c)) =
- let map (id, univs) = match univs with
- | None -> id
- | Some _ ->
- let loc = fst id in
- let msg =
- Pp.str "Assumptions with bound universes can only be defined one at a time." in
- user_err ?loc msg
- in
- (coe, (List.map map idl, c))
- in
- let l = List.map map l in
- do_assumptions_unbound_univs kind nl l
+ let evd = Evd.restrict_universe_context evd uvars in
+ let uctx = Evd.check_univ_decl ~poly:(pi2 kind) evd udecl in
+ let ubinders = Evd.universe_binders evd in
+ pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),t,imps) ->
+ let t = replace_vars subst t in
+ let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in
+ let subst' = List.map2
+ (fun (_,id) (c,u) -> (id, Universes.constr_of_global_univ (c,u)))
+ idl refs
+ in
+ subst'@subst, status' && status, next_uctx uctx)
+ ([], true, uctx) l)
(* 3a| Elimination schemes for mutual inductive definitions *)
@@ -576,7 +601,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 ~poly 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,_) ->
@@ -598,11 +623,12 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors
in
let univs =
- if poly then
+ match uctx with
+ | Polymorphic_const_entry uctx ->
if cum then
Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx)
else Polymorphic_ind_entry uctx
- else
+ | Monomorphic_const_entry uctx ->
Monomorphic_ind_entry uctx
in
(* Build the mutual inductive entry *)
@@ -617,7 +643,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 =
@@ -684,7 +710,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls =
let ind = (mind,i) in
let gr = IndRef ind in
maybe_declare_manual_implicits false gr indimpls;
- Universes.register_universe_binders gr pl;
+ Declare.declare_univ_binders gr pl;
List.iteri
(fun j impls ->
maybe_declare_manual_implicits false
@@ -1019,23 +1045,22 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let binders_rel = nf_evar_context !evdref binders_rel in
let binders = nf_evar_context !evdref binders in
let top_arity = Evarutil.nf_evar !evdref top_arity in
- let pl, plext = Option.cata
- (fun d -> d.univdecl_instance, d.univdecl_extensible_instance) ([],true) pl in
let hook, recname, typ =
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.check_univ_decl ~poly !evdref decl in
+ (*FIXME poly? *)
+ let ce = definition_entry ~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 +1193,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 ~poly 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 +1226,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 ~poly 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 *)
@@ -1239,7 +1266,7 @@ let collect_evars_of_term evd c ty =
Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
evars (Evd.from_ctx (Evd.evar_universe_context evd))
-let do_program_recursive local p fixkind fixl ntns =
+let do_program_recursive local poly fixkind fixl ntns =
let isfix = fixkind != Obligations.IsCoFixpoint in
let (env, rec_sign, pl, evd), fix, info =
interp_recursive isfix fixl ntns
@@ -1281,8 +1308,8 @@ let do_program_recursive local p fixkind fixl ntns =
end in
let ctx = Evd.evar_universe_context evd in
let kind = match fixkind with
- | Obligations.IsFixpoint _ -> (local, p, Fixpoint)
- | Obligations.IsCoFixpoint -> (local, p, CoFixpoint)
+ | Obligations.IsFixpoint _ -> (local, poly, Fixpoint)
+ | Obligations.IsCoFixpoint -> (local, poly, CoFixpoint)
in
Obligations.add_mutual_definitions defs ~kind ~univdecl:pl ctx ntns fixkind
diff --git a/vernac/command.mli b/vernac/command.mli
index fb99a717b9..a1f916c782 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -28,7 +28,7 @@ val do_constraint : polymorphic ->
val interp_definition :
Vernacexpr.universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map *
- Univdecls.universe_decl * Universes.universe_binders * Impargs.manual_implicits
+ Univdecls.universe_decl * Impargs.manual_implicits
val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option ->
local_binder_expr list -> red_expr option -> constr_expr ->
@@ -43,7 +43,7 @@ val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr opt
(** returns [false] if the assumption is neither local to a section,
nor in a module type and meant to be instantiated. *)
val declare_assumption : coercion_flag -> assumption_kind ->
- types Univ.in_universe_context_set ->
+ types in_constant_universes_entry ->
Universes.universe_binders -> Impargs.manual_implicits ->
bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located ->
global_reference * Univ.Instance.t * bool
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index c18744052e..dfac78c048 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -36,7 +36,7 @@ let declare_global_definition ident ce local k pl imps =
let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
let gr = ConstRef kn in
let () = maybe_declare_manual_implicits false gr imps in
- let () = Universes.register_universe_binders gr pl in
+ let () = Declare.declare_univ_binders gr pl in
let () = definition_message ident in
gr
@@ -49,6 +49,7 @@ let declare_definition ident (local, p, k) ce pl imps hook =
let () = definition_message ident in
let gr = VarRef ident in
let () = maybe_declare_manual_implicits false gr imps in
+ let () = Declare.declare_univ_binders gr pl in
let () = if Proof_global.there_are_pending_proofs () then
warn_definition_not_visible ident
in
@@ -57,7 +58,7 @@ let declare_definition ident (local, p, k) ce pl imps hook =
declare_global_definition ident ce local k pl imps in
Lemmas.call_hook fix_exn hook local r
-let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps =
- let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in
+let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
+ let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r))
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 01a87818a3..55f7c78616 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -15,5 +15,8 @@ val declare_definition : Id.t -> definition_kind ->
Safe_typing.private_constants Entries.definition_entry -> Universes.universe_binders -> Impargs.manual_implicits ->
Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
-val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.UContext.t -> Id.t ->
- Safe_typing.private_constants Entries.proof_output -> Constr.types -> Impargs.manual_implicits -> Globnames.global_reference
+val declare_fix : ?opaque:bool -> definition_kind ->
+ Universes.universe_binders -> Entries.constant_universes_entry ->
+ Id.t -> Safe_typing.private_constants Entries.proof_output ->
+ Constr.types -> Impargs.manual_implicits ->
+ Globnames.global_reference
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index c0ddc7e2ce..e4ca98749c 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -109,10 +109,10 @@ 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 =
- if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs
- else Monomorphic_const_entry univs
+ if Flags.is_universe_polymorphism ()
+ then Polymorphic_const_entry (Evd.to_universe_context ctx)
+ else Monomorphic_const_entry (Evd.universe_context_set ctx)
in
let kn = f id
(DefinitionEntry
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index a025bfff83..200c2260ed 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -49,7 +49,8 @@ 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
+ (* we get the right order somehow but surely it could be enforced in a better way *)
+ let uctx = UState.context 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)
@@ -176,7 +177,7 @@ let look_for_possibly_mutual_statements = function
(* Saving a goal *)
-let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
+let save ?export_seff id const uctx do_guard (locality,poly,kind) hook =
let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
try
let const = adjust_guardness_conditions const do_guard in
@@ -203,7 +204,7 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
(locality, ConstRef kn)
in
definition_message id;
- Option.iter (Universes.register_universe_binders r) pl;
+ Declare.declare_univ_binders r (UState.universe_binders uctx);
call_hook (fun exn -> exn) hook l r
with e when CErrors.noncritical e ->
let e = CErrors.push e in
@@ -223,7 +224,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 univs body opaq i (id,(t_i,(_,imps))) =
let t_i = norm t_i in
match body with
| None ->
@@ -231,7 +232,13 @@ let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t
| Discharge ->
let impl = false in (* copy values from Vernacentries *)
let k = IsAssumption Conjectural in
- let c = SectionLocalAssum ((t_i,Univ.ContextSet.of_context ctx),p,impl) in
+ let univs = match univs with
+ | Polymorphic_const_entry univs ->
+ (* What is going on here? *)
+ Univ.ContextSet.of_context univs
+ | Monomorphic_const_entry univs -> univs
+ in
+ let c = SectionLocalAssum ((t_i, univs),p,impl) in
let _ = declare_variable id (Lib.cwd(),c,k) in
(Discharge, VarRef id,imps)
| Local | Global ->
@@ -241,7 +248,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t
| Global -> false
| Discharge -> assert false
in
- let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in
+ let decl = (ParameterEntry (None,(t_i,univs),None), k) in
let kn = declare_constant id ~local decl in
(locality,ConstRef kn,imps))
| Some body ->
@@ -259,8 +266,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t
let body_i = body_i body in
match locality with
| Discharge ->
- let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p
- ~univs:ctx body_i in
+ let const = definition_entry ~types:t_i ~opaque:opaq ~univs body_i in
let c = SectionLocalDef const in
let _ = declare_variable id (Lib.cwd(), c, k) in
(Discharge,VarRef id,imps)
@@ -271,7 +277,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t
| Discharge -> assert false
in
let const =
- Declare.definition_entry ~types:t_i ~poly:p ~univs:ctx ~opaque:opaq body_i
+ Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i
in
let kn = declare_constant id ~local (DefinitionEntry const, k) in
(locality,ConstRef kn,imps)
@@ -280,17 +286,17 @@ let save_hook = ref ignore
let set_save_hook f = save_hook := f
let save_named ?export_seff proof =
- let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
- save ?export_seff id const cstrs pl do_guard persistence hook
+ let id,const,uctx,do_guard,persistence,hook = proof in
+ save ?export_seff id const uctx do_guard persistence hook
let check_anonymity id save_ident =
if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
user_err Pp.(str "This command can only be used for unnamed theorem.")
let save_anonymous ?export_seff proof save_ident =
- let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
+ let id,const,uctx,do_guard,persistence,hook = proof in
check_anonymity id save_ident;
- save ?export_seff save_ident const cstrs pl do_guard persistence hook
+ save ?export_seff save_ident const uctx do_guard persistence hook
(* Admitted *)
@@ -306,7 +312,7 @@ let admit (id,k,e) pl hook () =
| Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id
in
let () = assumption_message id in
- Option.iter (Universes.register_universe_binders (ConstRef kn)) pl;
+ Declare.declare_univ_binders (ConstRef kn) pl;
call_hook (fun exn -> exn) hook Global (ConstRef kn)
(* Starting a goal *)
@@ -324,8 +330,8 @@ let get_proof proof do_guard hook opacity =
let universe_proof_terminator compute_guard hook =
let open Proof_global in
make_terminator begin function
- | Admitted (id,k,pe,(ctx,pl)) ->
- admit (id,k,pe) pl (hook (Some ctx)) ();
+ | Admitted (id,k,pe,ctx) ->
+ admit (id,k,pe) (UState.universe_binders ctx) (hook (Some ctx)) ();
Feedback.feedback Feedback.AddedAxiom
| Proved (opaque,idopt,proof) ->
let is_opaque, export_seff = match opaque with
@@ -333,7 +339,7 @@ let universe_proof_terminator compute_guard hook =
| Vernacexpr.Opaque -> true, false
in
let proof = get_proof proof compute_guard
- (hook (Some (fst proof.Proof_global.universes))) is_opaque in
+ (hook (Some (proof.Proof_global.universes))) is_opaque in
begin match idopt with
| None -> save_named ~export_seff proof
| Some (_,id) -> save_anonymous ~export_seff proof id
@@ -411,7 +417,7 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook =
| (id,(t,(_,imps)))::other_thms ->
let hook ctx strength ref =
let ctx = match ctx with
- | None -> Evd.empty_evar_universe_context
+ | None -> UState.empty
| Some ctx -> ctx
in
let other_thms_data =
@@ -420,9 +426,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 body = Option.map norm body in
- List.map_i (save_remaining_recthms kind norm ctx binders body opaq) 1 other_thms in
+ let body = Option.map norm body in
+ let uctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in
+ List.map_i (save_remaining_recthms kind norm uctx 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;
@@ -453,9 +459,9 @@ let start_proof_com ?inference_hook kind thms hook =
let evd, nf = Evarutil.nf_evars_and_universes !evdref in
let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
let () =
- if not decl.Misctypes.univdecl_extensible_instance then
- ignore (Evd.universe_context evd ~names:decl.Misctypes.univdecl_instance ~extensible:false)
- else ()
+ let open Misctypes in
+ if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then
+ ignore (Evd.check_univ_decl ~poly:(pi2 kind) evd decl)
in
let evd =
if pi2 kind then evd
@@ -490,9 +496,9 @@ let save_proof ?proof = function
if const_entry_type = None then
user_err Pp.(str "Admitted requires an explicit statement");
let typ = Option.get const_entry_type in
- let ctx = Evd.evar_context_universe_context (fst universes) in
+ let ctx = UState.const_univ_entry ~poly:(pi2 k) universes in
let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
- Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes)
+ Admitted(id, k, (sec_vars, (typ, ctx), None), universes)
| None ->
let pftree = Proof_global.give_me_the_proof () in
let id, k, typ = Pfedit.current_proof_statement () in
@@ -512,12 +518,9 @@ let save_proof ?proof = function
Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def))
| _ -> 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 poly = pi2 k in
- let binders = if poly then Some binders else None in
- Admitted(id,k,(sec_vars, poly, (typ, ctx), None),
- (universes, binders))
+ let ctx = UState.check_univ_decl ~poly universes decl in
+ Admitted(id,k,(sec_vars, (typ, ctx), None), universes)
in
Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
| Vernacexpr.Proved (is_opaque,idopt) ->
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 1b1304db5b..a4854b4a6b 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -56,7 +56,7 @@ val standard_proof_terminator :
(** {6 ... } *)
(** A hook the next three functions pass to cook_proof *)
-val set_save_hook : (Proof.proof -> unit) -> unit
+val set_save_hook : (Proof.t -> unit) -> unit
val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
diff --git a/vernac/locality.ml b/vernac/locality.ml
index 681b1ab207..87b4116252 100644
--- a/vernac/locality.ml
+++ b/vernac/locality.ml
@@ -6,36 +6,14 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Decl_kinds
+
(** * Managing locality *)
let local_of_bool = function
- | true -> Decl_kinds.Local
- | false -> Decl_kinds.Global
-
-(** Extracting the locality flag *)
-
-(* Commands which supported an inlined Local flag *)
-
-let warn_deprecated_local_syntax =
- CWarnings.create ~name:"deprecated-local-syntax" ~category:"deprecated"
- (fun () ->
- Pp.strbrk "Deprecated syntax: use \"Local\" as a prefix.")
-
-let enforce_locality_full locality_flag local =
- let local =
- match locality_flag with
- | Some false when local ->
- CErrors.user_err Pp.(str "Cannot be simultaneously Local and Global.")
- | Some true when local ->
- CErrors.user_err Pp.(str "Use only prefix \"Local\".")
- | None ->
- if local then begin
- warn_deprecated_local_syntax ();
- Some true
- end else
- None
- | Some b -> Some b in
- local
+ | true -> Local
+ | false -> Global
+
(** Positioning locality for commands supporting discharging and export
outside of modules *)
@@ -48,15 +26,16 @@ let make_non_locality = function Some false -> false | _ -> true
let make_locality = function Some true -> true | _ -> false
-let enforce_locality locality_flag local =
- make_locality (enforce_locality_full locality_flag local)
+let enforce_locality_exp locality_flag discharge =
+ match locality_flag, discharge with
+ | Some b, NoDischarge -> local_of_bool b
+ | None, NoDischarge -> Global
+ | None, DoDischarge -> Discharge
+ | Some true, DoDischarge -> CErrors.user_err Pp.(str "Local not allowed in this case")
+ | Some false, DoDischarge -> CErrors.user_err Pp.(str "Global not allowed in this case")
-let enforce_locality_exp locality_flag local =
- match locality_flag, local with
- | None, Some local -> local
- | Some b, None -> local_of_bool b
- | None, None -> Decl_kinds.Global
- | Some _, Some _ -> CErrors.user_err Pp.(str "Local non allowed in this case")
+let enforce_locality locality_flag =
+ make_locality locality_flag
(* For commands whose default is to not discharge but to export:
Global in sections forces discharge, Global not in section is the default;
@@ -65,8 +44,8 @@ let enforce_locality_exp locality_flag local =
let make_section_locality =
function Some b -> b | None -> Lib.sections_are_opened ()
-let enforce_section_locality locality_flag local =
- make_section_locality (enforce_locality_full locality_flag local)
+let enforce_section_locality locality_flag =
+ make_section_locality locality_flag
(** Positioning locality for commands supporting export but not discharge *)
@@ -83,5 +62,5 @@ let make_module_locality = function
| Some true -> true
| None -> false
-let enforce_module_locality locality_flag local =
- make_module_locality (enforce_locality_full locality_flag local)
+let enforce_module_locality locality_flag =
+ make_module_locality locality_flag
diff --git a/vernac/locality.mli b/vernac/locality.mli
index bef66d8bc5..922538b233 100644
--- a/vernac/locality.mli
+++ b/vernac/locality.mli
@@ -8,10 +8,6 @@
(** * Managing locality *)
-(** Commands which supported an inlined Local flag *)
-
-val enforce_locality_full : bool option -> bool -> bool option
-
(** * Positioning locality for commands supporting discharging and export
outside of modules *)
@@ -22,16 +18,15 @@ val enforce_locality_full : bool option -> bool -> bool option
val make_locality : bool option -> bool
val make_non_locality : bool option -> bool
-val enforce_locality : bool option -> bool -> bool
-val enforce_locality_exp :
- bool option -> Decl_kinds.locality option -> Decl_kinds.locality
+val enforce_locality_exp : bool option -> Decl_kinds.discharge -> Decl_kinds.locality
+val enforce_locality : bool option -> bool
(** For commands whose default is to not discharge but to export:
Global in sections forces discharge, Global not in section is the default;
Local in sections is the default, Local not in section forces non-export *)
val make_section_locality : bool option -> bool
-val enforce_section_locality : bool option -> bool -> bool
+val enforce_section_locality : bool option -> bool
(** * Positioning locality for commands supporting export but not discharge *)
@@ -40,4 +35,4 @@ val enforce_section_locality : bool option -> bool -> bool
Local in sections is the default, Local not in section forces non-export *)
val make_module_locality : bool option -> bool
-val enforce_module_locality : bool option -> bool -> bool
+val enforce_module_locality : bool option -> bool
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index a44de66e96..24d6649515 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -155,7 +155,7 @@ let evar_dependencies evm oev =
let evi = Evd.find evm ev in
let deps' = evars_of_filtered_evar_info evi in
if Evar.Set.mem oev deps' then
- invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ string_of_existential oev)
+ invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ Pp.string_of_ppcmds @@ Evar.print oev)
else Evar.Set.union deps' s)
deps deps
in
@@ -164,7 +164,7 @@ let evar_dependencies evm oev =
if Evar.Set.equal deps deps' then deps
else aux deps'
in aux (Evar.Set.singleton oev)
-
+
let move_after (id, ev, deps as obl) l =
let rec aux restdeps = function
| (id', _, _) as obl' :: tl ->
@@ -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 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 typ = nf typ in
+ let body = nf body in
+ let uvars = Univ.LSet.union (Univops.universes_of_constr typ) (Univops.universes_of_constr body) in
+ let uctx = UState.restrict prg.prg_ctx uvars in
+ let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in
+ let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in
let () = progmap_remove prg in
- let cst =
- DeclareDef.declare_definition prg.prg_name
- prg.prg_kind ce [] 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 uctx 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 uctx; r))
let rec lam_index n t acc =
match Constr.kind t with
@@ -552,9 +549,9 @@ let declare_mutual_definition l =
mk_proof (mkCoFix (i,fixdecls))) 0 l
in
(* Declare the recursive definitions *)
- let ctx = Evd.evar_context_universe_context first.prg_ctx in
+ let univs = UState.const_univ_entry ~poly first.prg_ctx in
let fix_exn = Hook.get get_fix_exn () in
- let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) [] ctx)
+ let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders univs)
fixnames fixdecls fixtypes fiximps in
(* Declare notations *)
List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
@@ -636,12 +633,11 @@ let declare_obligation prg obl body ty uctx =
shrink_body body ty else [], body, ty, [||]
in
let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
- let univs = if poly then Polymorphic_const_entry uctx else Monomorphic_const_entry uctx in
let ce =
{ const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body;
const_entry_secctx = None;
const_entry_type = ty;
- const_entry_universes = univs;
+ const_entry_universes = uctx;
const_entry_opaque = opaque;
const_entry_inline_code = false;
const_entry_feedback = None;
@@ -650,13 +646,15 @@ let declare_obligation prg obl body ty uctx =
let constant = Declare.declare_constant obl.obl_name ~local:true
(DefinitionEntry ce,IsProof Property)
in
- if not opaque then add_hint (Locality.make_section_locality None) prg constant;
- definition_message obl.obl_name;
- true, { obl with obl_body =
- if poly then
- Some (DefinedObl (constant, Univ.UContext.instance uctx))
- else
- Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) }
+ if not opaque then add_hint (Locality.make_section_locality None) prg constant;
+ definition_message obl.obl_name;
+ let body = match uctx with
+ | Polymorphic_const_entry uctx ->
+ Some (DefinedObl (constant, Univ.UContext.instance uctx))
+ | Monomorphic_const_entry _ ->
+ Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx))
+ in
+ true, { obl with obl_body = body }
let init_prog_info ?(opaque = false) sign n udecl b t ctx deps fixkind
notations obls impls kind reduce hook =
@@ -830,49 +828,63 @@ let obligation_terminator name num guard hook auto pf =
match pf with
| Admitted _ -> apply_terminator term pf
| Proved (opq, id, proof) ->
- if not !shrink_obligations then apply_terminator term pf
- else
- let (_, (entry, uctx, _)) = Pfedit.cook_this_proof proof in
- let env = Global.env () in
- let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
- let ty = entry.Entries.const_entry_type in
- let (body, cstr), () = Future.force entry.Entries.const_entry_body in
- let sigma = Evd.from_ctx (fst uctx) in
- let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
- Inductiveops.control_only_guard (Global.env ()) body;
- (** Declare the obligation ourselves and drop the hook *)
- let prg = get_info (ProgMap.find name !from_prg) in
- (** Ensure universes are substituted properly in body and type *)
- let body = EConstr.to_constr sigma (EConstr.of_constr body) in
- let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in
- let ctx = Evd.evar_universe_context sigma in
- let prg = { prg with prg_ctx = ctx } in
- let obls, rem = prg.prg_obligations in
- let obl = obls.(num) in
- let status =
- match obl.obl_status, opq with
- | (_, Evar_kinds.Expand), Vernacexpr.Opaque -> err_not_transp ()
- | (true, _), Vernacexpr.Opaque -> err_not_transp ()
- | (false, _), Vernacexpr.Opaque -> Evar_kinds.Define true
- | (_, Evar_kinds.Define true), Vernacexpr.Transparent -> Evar_kinds.Define false
- | (_, status), Vernacexpr.Transparent -> status
- in
- let obl = { obl with obl_status = false, status } in
- let uctx = Evd.evar_context_universe_context ctx in
- let (_, obl) = declare_obligation prg obl body ty uctx in
- let obls = Array.copy obls in
- let _ = obls.(num) <- obl in
- try
+ let (_, (entry, uctx, _)) = Pfedit.cook_this_proof proof in
+ let env = Global.env () in
+ let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
+ let ty = entry.Entries.const_entry_type in
+ let (body, cstr), () = Future.force entry.Entries.const_entry_body in
+ let sigma = Evd.from_ctx uctx in
+ let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
+ Inductiveops.control_only_guard (Global.env ()) body;
+ (** Declare the obligation ourselves and drop the hook *)
+ let prg = get_info (ProgMap.find name !from_prg) in
+ (** Ensure universes are substituted properly in body and type *)
+ let body = EConstr.to_constr sigma (EConstr.of_constr body) in
+ let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in
+ let ctx = Evd.evar_universe_context sigma in
+ let obls, rem = prg.prg_obligations in
+ let obl = obls.(num) in
+ let status =
+ match obl.obl_status, opq with
+ | (_, Evar_kinds.Expand), Vernacexpr.Opaque -> err_not_transp ()
+ | (true, _), Vernacexpr.Opaque -> err_not_transp ()
+ | (false, _), Vernacexpr.Opaque -> Evar_kinds.Define true
+ | (_, Evar_kinds.Define true), Vernacexpr.Transparent ->
+ Evar_kinds.Define false
+ | (_, status), Vernacexpr.Transparent -> status
+ in
+ let obl = { obl with obl_status = false, status } in
+ let ctx =
+ if pi2 prg.prg_kind then ctx
+ else UState.union prg.prg_ctx ctx
+ in
+ let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in
+ let (_, obl) = declare_obligation prg obl body ty uctx in
+ let obls = Array.copy obls in
+ let _ = obls.(num) <- obl in
+ let prg_ctx =
+ if pi2 (prg.prg_kind) then (* Polymorphic *)
+ (** We merge the new universes and constraints of the
+ polymorphic obligation with the existing ones *)
+ UState.union prg.prg_ctx ctx
+ else
+ (** The first obligation declares the univs of the constant,
+ each subsequent obligation declares its own additional
+ universes and constraints if any *)
+ UState.make (Global.universes ())
+ in
+ let prg = { prg with prg_ctx } in
+ try
ignore (update_obls prg obls (pred rem));
if pred rem > 0 then
begin
- let deps = dependencies obls num in
- if not (Int.Set.is_empty deps) then
- ignore (auto (Some name) None deps)
- end
- with e when CErrors.noncritical e ->
- let e = CErrors.push e in
- pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e))
+ let deps = dependencies obls num in
+ if not (Int.Set.is_empty deps) then
+ ignore (auto (Some name) None deps)
+ end
+ with e when CErrors.noncritical e ->
+ let e = CErrors.push e in
+ pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e))
let obligation_hook prg obl num auto ctx' _ gr =
let obls, rem = prg.prg_obligations in
@@ -893,7 +905,8 @@ 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
+ (* We get the right order somehow, but surely it could be enforced in a clearer way. *)
+ let uctx = UState.context ctx' in
Univ.UContext.instance uctx, ctx'
in
let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in
@@ -969,13 +982,16 @@ and solve_obligation_by_tac prg obls i tac =
let evd = Evd.from_ctx prg.prg_ctx in
let evd = Evd.update_sigma_env evd (Global.env ()) in
let t, ty, ctx =
- solve_by_tac obl.obl_name (evar_of_obligation obl) tac
- (pi2 prg.prg_kind) (Evd.evar_universe_context evd)
- in
- let uctx = Evd.evar_context_universe_context ctx in
- let prg = {prg with prg_ctx = ctx} in
- let def, obl' = declare_obligation prg obl t ty uctx in
- obls.(i) <- obl';
+ solve_by_tac obl.obl_name (evar_of_obligation obl) tac
+ (pi2 prg.prg_kind) (Evd.evar_universe_context evd)
+ in
+ let uctx = if pi2 prg.prg_kind
+ then Polymorphic_const_entry (UState.context ctx)
+ else Monomorphic_const_entry (UState.context_set ctx)
+ in
+ let prg = {prg with prg_ctx = ctx} in
+ let def, obl' = declare_obligation prg obl t ty uctx in
+ obls.(i) <- obl';
if def && not (pi2 prg.prg_kind) then (
(* Declare the term constraints with the first obligation only *)
let evd = Evd.from_env (Global.env ()) in
@@ -1123,9 +1139,9 @@ let admit_prog prg =
match x.obl_body with
| None ->
let x = subst_deps_obl obls x in
- let ctx = Evd.evar_context_universe_context prg.prg_ctx in
+ let ctx = Monomorphic_const_entry (UState.context_set prg.prg_ctx) in
let kn = Declare.declare_constant x.obl_name ~local:true
- (ParameterEntry (None,false,(x.obl_type,ctx),None), IsAssumption Conjectural)
+ (ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural)
in
assumption_message x.obl_name;
obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) }
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 481faadb8e..0602e52e9a 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -32,7 +32,7 @@ val eterm_obligations : env -> Id.t -> evar_map -> int ->
(* Existential key, obl. name, type as product,
location of the original evar, associated tactic,
status and dependencies as indexes into the array *)
- * ((existential_key * Id.t) list * ((Id.t -> constr) -> constr -> constr)) *
+ * ((Evar.t * Id.t) list * ((Id.t -> constr) -> constr -> constr)) *
constr * types
(* Translations from existential identifiers to obligation identifiers
and for terms with existentials to closed terms, given a
diff --git a/vernac/record.ml b/vernac/record.ml
index f09b570489..1cdc538b5b 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -95,7 +95,7 @@ let binder_of_decl = function
let binders_of_decls = List.map binder_of_decl
-let typecheck_params_and_fields finite def id pl t ps nots fs =
+let typecheck_params_and_fields finite def id poly pl t ps nots fs =
let env0 = Global.env () in
let evd, decl = Univdecls.interp_univ_decl_opt env0 pl in
let evars = ref evd in
@@ -167,10 +167,11 @@ let typecheck_params_and_fields finite def id pl t ps nots fs =
let newps = List.map (EConstr.to_rel_decl evars) newps in
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 univs = Evd.check_univ_decl ~poly 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
@@ -265,12 +266,14 @@ let warn_non_primitive_record =
strbrk" could not be defined as a primitive record")))
(* We build projections *)
-let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields =
+let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers ubinders fieldimpls fields =
let env = Global.env() in
let (mib,mip) = Global.lookup_inductive indsp in
let poly = Declareops.inductive_is_polymorphic mib in
- let ctx = Univ.AUContext.repr (Declareops.inductive_polymorphic_context mib) in
- let u = Univ.UContext.instance ctx in
+ let u = match ctx with
+ | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx
+ | Monomorphic_const_entry ctx -> Univ.Instance.empty
+ in
let paramdecls = Inductive.inductive_paramdecls (mib, u) in
let indu = indsp, u in
let r = mkIndU (indsp,u) in
@@ -304,9 +307,11 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
let kn, term =
if is_local_assum decl && primitive then
(** Already defined in the kernel silently *)
- let kn = destConstRef (Nametab.locate (Libnames.qualid_of_ident fid)) in
- Declare.definition_message fid;
- kn, mkProj (Projection.make kn false,mkRel 1)
+ let gr = Nametab.locate (Libnames.qualid_of_ident fid) in
+ let kn = destConstRef gr in
+ Declare.definition_message fid;
+ Universes.register_universe_binders gr ubinders;
+ kn, mkProj (Projection.make kn false,mkRel 1)
else
let ccl = subst_projection fid subst ti in
let body = match decl with
@@ -325,16 +330,12 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
let projtyp =
it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
try
- let univs =
- if poly then Polymorphic_const_entry ctx
- else Monomorphic_const_entry ctx
- in
let entry = {
const_entry_body =
Future.from_val (Safe_typing.mk_pure_proof proj);
const_entry_secctx = None;
const_entry_type = Some projtyp;
- const_entry_universes = univs;
+ const_entry_universes = ctx;
const_entry_opaque = false;
const_entry_inline_code = false;
const_entry_feedback = None } in
@@ -343,8 +344,9 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
let constr_fip =
let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
applist (mkConstU (kn,u),proj_args)
- in
- Declare.definition_message fid;
+ in
+ Declare.definition_message fid;
+ Universes.register_universe_binders (ConstRef kn) ubinders;
kn, constr_fip
with Type_errors.TypeError (ctx,te) ->
raise (NotDefinable (BadTypedProj (fid,ctx,te)))
@@ -382,17 +384,20 @@ let structure_signature ctx =
open Typeclasses
-let declare_structure finite univs id idbuild paramimpls params arity template
+let declare_structure finite ubinders univs id idbuild paramimpls params arity template
fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign =
let nparams = List.length params and nfields = List.length fields in
let args = Context.Rel.to_extended_list mkRel nfields params in
let ind = applist (mkRel (1+nparams+nfields), args) in
let type_constructor = it_mkProd_or_LetIn ind fields in
- let poly, ctx =
+ let template, ctx =
match univs with
- | Monomorphic_ind_entry ctx -> false, ctx
- | Polymorphic_ind_entry ctx -> true, ctx
- | Cumulative_ind_entry cumi -> true, (Univ.CumulativityInfo.univ_context cumi)
+ | Monomorphic_ind_entry ctx ->
+ template, Monomorphic_const_entry Univ.ContextSet.empty
+ | Polymorphic_ind_entry ctx ->
+ false, Polymorphic_const_entry ctx
+ | Cumulative_ind_entry cumi ->
+ false, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi)
in
let binder_name =
match name with
@@ -402,7 +407,7 @@ let declare_structure finite univs id idbuild paramimpls params arity template
let mie_ind =
{ mind_entry_typename = id;
mind_entry_arity = arity;
- mind_entry_template = not poly && template;
+ mind_entry_template = template;
mind_entry_consnames = [idbuild];
mind_entry_lc = [type_constructor] }
in
@@ -416,27 +421,21 @@ let declare_structure finite univs id idbuild paramimpls params arity template
}
in
let mie =
- if poly then
- begin
+ match ctx with
+ | Polymorphic_const_entry ctx ->
let env = Global.env () in
let env' = Environ.push_context ctx env in
let evd = Evd.from_env env' in
Inductiveops.infer_inductive_subtyping env' evd mie
- end
- else
+ | Monomorphic_const_entry _ ->
mie
in
- let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in
+ let kn = Command.declare_mutual_inductive_with_eliminations mie ubinders [(paramimpls,[])] in
let rsp = (kn,0) in (* This is ind path of idstruc *)
let cstr = (rsp,1) in
- let fields =
- if poly then
- let subst, _ = Univ.abstract_universes ctx in
- Context.Rel.map (fun c -> Vars.subst_univs_level_constr subst c) fields
- else fields
- in
- let kinds,sp_projs = declare_projections rsp ~kind binder_name coers fieldimpls fields in
+ let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name coers ubinders fieldimpls fields in
let build = ConstructRef cstr in
+ let poly = match ctx with | Polymorphic_const_entry _ -> true | Monomorphic_const_entry _ -> false in
let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs);
rsp
@@ -450,7 +449,7 @@ let implicits_of_context ctx =
in ExplByPos (i, explname), (true, true, true))
1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
-let declare_class finite def cum poly ctx id idbuild paramimpls params arity
+let declare_class finite def cum ubinders univs id idbuild paramimpls params arity
template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign =
let fieldimpls =
(* Make the class implicit in the projections, and the params if applicable. *)
@@ -465,27 +464,29 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity
let class_body = it_mkLambda_or_LetIn field params in
let class_type = it_mkProd_or_LetIn arity params in
let class_entry =
- Declare.definition_entry ~types:class_type ~poly ~univs:ctx class_body in
+ Declare.definition_entry ~types:class_type ~univs class_body in
let cst = Declare.declare_constant (snd id)
(DefinitionEntry class_entry, IsDefinition Definition)
in
- let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in
+ let cstu = (cst, match univs with
+ | Polymorphic_const_entry univs -> Univ.UContext.instance univs
+ | Monomorphic_const_entry _ -> Univ.Instance.empty)
+ in
let inst_type = appvectc (mkConstU cstu)
(Termops.rel_vect 0 (List.length params)) in
let proj_type =
it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in
let proj_body =
it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in
- let proj_entry =
- Declare.definition_entry ~types:proj_type ~poly
- ~univs:(if poly then ctx else Univ.UContext.empty) proj_body
- in
+ let proj_entry = Declare.definition_entry ~types:proj_type ~univs proj_body in
let proj_cst = Declare.declare_constant proj_name
(DefinitionEntry proj_entry, IsDefinition Definition)
in
let cref = ConstRef cst in
Impargs.declare_manual_implicits false cref [paramimpls];
+ Universes.register_universe_binders cref ubinders;
Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls];
+ Universes.register_universe_binders (ConstRef proj_cst) ubinders;
Classes.set_typeclass_transparency (EvalConstRef cst) false false;
let sub = match List.hd coers with
| Some b -> Some ((if b then Backward else Forward), List.hd priorities)
@@ -494,15 +495,16 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity
cref, [Name proj_name, sub, Some proj_cst]
| _ ->
let univs =
- if poly then
+ match univs with
+ | Polymorphic_const_entry univs ->
if cum then
- Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context ctx)
+ Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs)
else
- Polymorphic_ind_entry ctx
- else
- Monomorphic_ind_entry ctx
+ Polymorphic_ind_entry univs
+ | Monomorphic_const_entry univs ->
+ Monomorphic_ind_entry univs
in
- let ind = declare_structure BiFinite univs (snd id) idbuild paramimpls
+ let ind = declare_structure BiFinite ubinders univs (snd id) idbuild paramimpls
params arity template fieldimpls fields
~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign
in
@@ -523,13 +525,15 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity
params, params
in
let univs, ctx_context, fields =
- if poly then
- let usubst, auctx = Univ.abstract_universes ctx in
+ match univs with
+ | Polymorphic_const_entry univs ->
+ let usubst, auctx = Univ.abstract_universes univs in
let map c = Vars.subst_univs_level_constr usubst c in
let fields = Context.Rel.map map fields in
let ctx_context = on_snd (fun d -> Context.Rel.map map d) ctx_context in
auctx, ctx_context, fields
- else Univ.AUContext.empty, ctx_context, fields
+ | Monomorphic_const_entry _ ->
+ Univ.AUContext.empty, ctx_context, fields
in
let k =
{ cl_univs = univs;
@@ -605,14 +609,14 @@ 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, univs, 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
+ typecheck_params_and_fields finite (kind = Class true) idstruc poly pl s ps notations fs) () in
let sign = structure_signature (fields@params) in
let gr = match kind with
| Class def ->
let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in
- let gr = declare_class finite def cum poly ctx (loc,idstruc) idbuild
+ let gr = declare_class finite def cum pl univs (loc,idstruc) idbuild
implpars params arity template implfs fields is_coe coers priorities sign in
gr
| _ ->
@@ -621,18 +625,19 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
(succ (List.length params)) impls) implfs
in
let univs =
- if poly then
+ match univs with
+ | Polymorphic_const_entry univs ->
if cum then
- Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context ctx)
+ Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs)
else
- Polymorphic_ind_entry ctx
- else
- Monomorphic_ind_entry ctx
+ Polymorphic_ind_entry univs
+ | Monomorphic_const_entry univs ->
+ Monomorphic_ind_entry univs
in
- let ind = declare_structure finite univs idstruc
+ let ind = declare_structure finite pl univs idstruc
idbuild implpars params arity template implfs
fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in
IndRef ind
in
- Universes.register_universe_binders gr pl;
+ Declare.declare_univ_binders gr pl;
gr
diff --git a/vernac/record.mli b/vernac/record.mli
index 33c2fba89c..9fdd5e1c46 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -7,36 +7,12 @@
(************************************************************************)
open Names
-open Constr
open Vernacexpr
open Constrexpr
-open Impargs
open Globnames
val primitive_flag : bool ref
-(** [declare_projections ref name coers params fields] declare projections of
- record [ref] (if allowed) using the given [name] as argument, and put them
- as coercions accordingly to [coers]; it returns the absolute names of projections *)
-
-val declare_projections :
- inductive -> ?kind:Decl_kinds.definition_object_kind -> Id.t ->
- coercion_flag list -> manual_explicitation list list -> Context.Rel.t ->
- (Name.t * bool) list * Constant.t option list
-
-val declare_structure :
- Decl_kinds.recursivity_kind ->
- Entries.inductive_universes ->
- Id.t -> Id.t ->
- manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *)
- bool (** template arity ? *) ->
- Impargs.manual_explicitation list list -> Context.Rel.t -> (** fields *)
- ?kind:Decl_kinds.definition_object_kind -> ?name:Id.t ->
- bool -> (** coercion? *)
- bool list -> (** field coercions *)
- Evd.evar_map ->
- inductive
-
val definition_structure :
inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic *
Decl_kinds.recursivity_kind * ident_decl with_coercion * local_binder_expr list *
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index bdd351901d..63768d9b88 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -29,6 +29,7 @@ open Redexpr
open Lemmas
open Misctypes
open Locality
+open Vernacinterp
module NamedDecl = Context.Named.Declaration
@@ -185,8 +186,8 @@ let print_module r =
try
let globdir = Nametab.locate_dir qid in
match globdir with
- DirModule (dirpath,(mp,_)) ->
- Feedback.msg_notice (Printmod.print_module (Printmod.printable_body dirpath) mp)
+ DirModule { obj_dir; obj_mp; _ } ->
+ Feedback.msg_notice (Printmod.print_module (Printmod.printable_body obj_dir) obj_mp)
| _ -> raise Not_found
with
Not_found -> Feedback.msg_error (str"Unknown Module " ++ pr_qualid qid)
@@ -408,8 +409,8 @@ let dump_global r =
(**********)
(* Syntax *)
-let vernac_syntax_extension locality local infix l =
- let local = enforce_module_locality locality local in
+let vernac_syntax_extension atts infix l =
+ let local = enforce_module_locality atts.locality in
if infix then Metasyntax.check_infix_modifiers (snd l);
Metasyntax.add_syntax_extension local l
@@ -420,20 +421,20 @@ let vernac_delimiters sc = function
let vernac_bind_scope sc cll =
Metasyntax.add_class_scope sc (List.map scope_class_of_qualid cll)
-let vernac_open_close_scope locality local (b,s) =
- let local = enforce_section_locality locality local in
+let vernac_open_close_scope ~atts (b,s) =
+ let local = enforce_section_locality atts.locality in
Notation.open_close_scope (local,b,s)
-let vernac_arguments_scope locality r scl =
- let local = make_section_locality locality in
+let vernac_arguments_scope ~atts r scl =
+ let local = make_section_locality atts.locality in
Notation.declare_arguments_scope local (smart_global r) scl
-let vernac_infix locality local =
- let local = enforce_module_locality locality local in
+let vernac_infix ~atts =
+ let local = enforce_module_locality atts.locality in
Metasyntax.add_infix local (Global.env())
-let vernac_notation locality local =
- let local = enforce_module_locality locality local in
+let vernac_notation ~atts =
+ let local = enforce_module_locality atts.locality in
Metasyntax.add_notation local (Global.env())
(***********)
@@ -471,33 +472,33 @@ let vernac_definition_hook p = function
| SubClass -> Class.add_subclass_hook p
| _ -> no_hook
-let vernac_definition locality p (local,k) ((loc,id as lid),pl) def =
- let local = enforce_locality_exp locality local in
- let hook = vernac_definition_hook p k in
+let vernac_definition ~atts discharge kind ((loc,id as lid),pl) def =
+ let local = enforce_locality_exp atts.locality discharge in
+ let hook = vernac_definition_hook atts.polymorphic kind in
let () = match local with
| Discharge -> Dumpglob.dump_definition lid true "var"
| Local | Global -> Dumpglob.dump_definition lid false "def"
in
(match def with
| ProveBody (bl,t) -> (* local binders, typ *)
- start_proof_and_print (local,p,DefinitionBody k)
+ start_proof_and_print (local, atts.polymorphic, DefinitionBody kind)
[Some (lid,pl), (bl,t)] hook
| DefineBody (bl,red_option,c,typ_opt) ->
- let red_option = match red_option with
+ let red_option = match red_option with
| None -> None
| Some r ->
- let sigma, env= Pfedit.get_current_context () in
+ let sigma, env = Pfedit.get_current_context () in
Some (snd (Hook.get f_interp_redexp env sigma r)) in
- do_definition id (local,p,k) pl bl red_option c typ_opt hook)
+ do_definition id (local, atts.polymorphic, kind) pl bl red_option c typ_opt hook)
-let vernac_start_proof locality p kind l =
- let local = enforce_locality_exp locality None in
+let vernac_start_proof ~atts kind l =
+ let local = enforce_locality_exp atts.locality NoDischarge in
if Dumpglob.dump () then
List.iter (fun (id, _) ->
match id with
| Some (lid,_) -> Dumpglob.dump_definition lid false "prf"
| None -> ()) l;
- start_proof_and_print (local, p, Proof kind) l no_hook
+ start_proof_and_print (local, atts.polymorphic, Proof kind) l no_hook
let vernac_end_proof ?proof = function
| Admitted -> save_proof ?proof Admitted
@@ -510,10 +511,10 @@ let vernac_exact_proof c =
save_proof (Vernacexpr.(Proved(Opaque,None)));
if not status then Feedback.feedback Feedback.AddedAxiom
-let vernac_assumption locality poly (local, kind) l nl =
- let local = enforce_locality_exp locality local in
+let vernac_assumption ~atts discharge kind l nl =
+ let local = enforce_locality_exp atts.locality discharge in
let global = local == Global in
- let kind = local, poly, kind in
+ let kind = local, atts.polymorphic, kind in
List.iter (fun (is_coe,(idl,c)) ->
if Dumpglob.dump () then
List.iter (fun (lid, _) ->
@@ -553,8 +554,8 @@ let vernac_record cum k poly finite struc binders sort nameopt cfs =
then the type is declared private (as per the [Private] keyword). [finite]
indicates whether the type is inductive, co-inductive or
neither. *)
-let vernac_inductive cum poly lo finite indl =
- let is_cumulative = should_treat_as_cumulative cum poly in
+let vernac_inductive ~atts cum lo finite indl =
+ let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in
if Dumpglob.dump () then
List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) ->
match cstrs with
@@ -571,13 +572,13 @@ let vernac_inductive cum poly lo finite indl =
user_err Pp.(str "The Variant keyword does not support syntax { ... }.")
| [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] ->
vernac_record cum (match b with Class _ -> Class false | _ -> b)
- poly finite id bl c oc fs
+ atts.polymorphic finite id bl c oc fs
| [ ( id , bl , c , Class _, Constructors [l]), [] ] ->
let f =
let (coe, ((loc, id), ce)) = l in
let coe' = if coe then Some true else None in
(((coe', AssumExpr ((loc, Name id), ce)), None), [])
- in vernac_record cum (Class true) poly finite id bl c None [f]
+ in vernac_record cum (Class true) atts.polymorphic finite id bl c None [f]
| [ ( _ , _, _, Class _, Constructors _), [] ] ->
user_err Pp.(str "Inductive classes not supported")
| [ ( id , bl , c , Class _, _), _ :: _ ] ->
@@ -591,19 +592,19 @@ let vernac_inductive cum poly lo finite indl =
| _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.")
in
let indl = List.map unpack indl in
- do_mutual_inductive indl is_cumulative poly lo finite
+ do_mutual_inductive indl is_cumulative atts.polymorphic lo finite
-let vernac_fixpoint locality poly local l =
- let local = enforce_locality_exp locality local in
+let vernac_fixpoint ~atts discharge l =
+ let local = enforce_locality_exp atts.locality discharge in
if Dumpglob.dump () then
List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
- do_fixpoint local poly l
+ do_fixpoint local atts.polymorphic l
-let vernac_cofixpoint locality poly local l =
- let local = enforce_locality_exp locality local in
+let vernac_cofixpoint ~atts discharge l =
+ let local = enforce_locality_exp atts.locality discharge in
if Dumpglob.dump () then
List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
- do_cofixpoint local poly l
+ do_cofixpoint local atts.polymorphic l
let vernac_scheme l =
if Dumpglob.dump () then
@@ -621,19 +622,19 @@ let vernac_combined_scheme lid l =
List.iter (fun lid -> dump_global (Misctypes.AN (Ident lid))) l);
Indschemes.do_combined_scheme lid l
-let vernac_universe loc poly l =
- if poly && not (Lib.sections_are_opened ()) then
- user_err ?loc ~hdr:"vernac_universe"
+let vernac_universe ~atts l =
+ if atts.polymorphic && not (Lib.sections_are_opened ()) then
+ user_err ?loc:atts.loc ~hdr:"vernac_universe"
(str"Polymorphic universes can only be declared inside sections, " ++
str "use Monomorphic Universe instead");
- do_universe poly l
+ do_universe atts.polymorphic l
-let vernac_constraint loc poly l =
- if poly && not (Lib.sections_are_opened ()) then
- user_err ?loc ~hdr:"vernac_constraint"
+let vernac_constraint ~atts l =
+ if atts.polymorphic && not (Lib.sections_are_opened ()) then
+ user_err ?loc:atts.loc ~hdr:"vernac_constraint"
(str"Polymorphic universe constraints can only be declared"
++ str " inside sections, use Monomorphic Constraint instead");
- do_constraint poly l
+ do_constraint atts.polymorphic l
(**********************)
(* Modules *)
@@ -811,32 +812,32 @@ let vernac_require from import qidl =
let vernac_canonical r =
Recordops.declare_canonical_structure (smart_global r)
-let vernac_coercion locality poly local ref qids qidt =
- let local = enforce_locality locality local in
+let vernac_coercion ~atts ref qids qidt =
+ let local = enforce_locality atts.locality in
let target = cl_of_qualid qidt in
let source = cl_of_qualid qids in
let ref' = smart_global ref in
- Class.try_add_new_coercion_with_target ref' ~local poly ~source ~target;
+ Class.try_add_new_coercion_with_target ref' ~local atts.polymorphic ~source ~target;
Flags.if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion")
-let vernac_identity_coercion locality poly local id qids qidt =
- let local = enforce_locality locality local in
+let vernac_identity_coercion ~atts id qids qidt =
+ let local = enforce_locality atts.locality in
let target = cl_of_qualid qidt in
let source = cl_of_qualid qids in
- Class.try_add_new_identity_coercion id ~local poly ~source ~target
+ Class.try_add_new_identity_coercion id ~local atts.polymorphic ~source ~target
(* Type classes *)
-let vernac_instance abst locality poly sup inst props pri =
- let global = not (make_section_locality locality) in
+let vernac_instance ~atts abst sup inst props pri =
+ let global = not (make_section_locality atts.locality) in
Dumpglob.dump_constraint inst false "inst";
- ignore(Classes.new_instance ~abstract:abst ~global poly sup inst props pri)
+ ignore(Classes.new_instance ~abstract:abst ~global atts.polymorphic sup inst props pri)
-let vernac_context poly l =
- if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom
+let vernac_context ~atts l =
+ if not (Classes.context atts.polymorphic l) then Feedback.feedback Feedback.AddedAxiom
-let vernac_declare_instances locality insts =
- let glob = not (make_section_locality locality) in
+let vernac_declare_instances ~atts insts =
+ let glob = not (make_section_locality atts.locality) in
List.iter (fun (id, info) -> Classes.existing_instance glob id (Some info)) insts
let vernac_declare_class id =
@@ -904,8 +905,8 @@ let vernac_remove_loadpath path =
let vernac_add_ml_path isrec path =
(if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir) (expand path)
-let vernac_declare_ml_module locality l =
- let local = make_locality locality in
+let vernac_declare_ml_module ~atts l =
+ let local = make_locality atts.locality in
Mltop.declare_ml_modules local (List.map expand l)
let vernac_chdir = function
@@ -938,25 +939,25 @@ let vernac_restore_state file =
(************)
(* Commands *)
-let vernac_create_hintdb locality id b =
- let local = make_module_locality locality in
+let vernac_create_hintdb ~atts id b =
+ let local = make_module_locality atts.locality in
Hints.create_hint_db local id full_transparent_state b
-let vernac_remove_hints locality dbs ids =
- let local = make_module_locality locality in
+let vernac_remove_hints ~atts dbs ids =
+ let local = make_module_locality atts.locality in
Hints.remove_hints local dbs (List.map Smartlocate.global_with_alias ids)
-let vernac_hints locality poly local lb h =
- let local = enforce_module_locality locality local in
- Hints.add_hints local lb (Hints.interp_hints poly h)
+let vernac_hints ~atts lb h =
+ let local = enforce_module_locality atts.locality in
+ Hints.add_hints local lb (Hints.interp_hints atts.polymorphic h)
-let vernac_syntactic_definition locality lid x local y =
+let vernac_syntactic_definition ~atts lid x y =
Dumpglob.dump_definition lid false "syndef";
- let local = enforce_module_locality locality local in
+ let local = enforce_module_locality atts.locality in
Metasyntax.add_syntactic_definition (Global.env()) (snd lid) x local y
-let vernac_declare_implicits locality r l =
- let local = make_section_locality locality in
+let vernac_declare_implicits ~atts r l =
+ let local = make_section_locality atts.locality in
match l with
| [] ->
Impargs.declare_implicits local (smart_global r)
@@ -976,7 +977,7 @@ let warn_arguments_assert =
(* [nargs_for_red] is the number of arguments required to trigger reduction,
[args] is the main list of arguments statuses,
[more_implicits] is a list of extra lists of implicit statuses *)
-let vernac_arguments locality reference args more_implicits nargs_for_red flags =
+let vernac_arguments ~atts reference args more_implicits nargs_for_red flags =
let assert_flag = List.mem `Assert flags in
let rename_flag = List.mem `Rename flags in
let clear_scopes_flag = List.mem `ClearScopes flags in
@@ -1184,7 +1185,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
(* Actions *)
if renaming_specified then begin
- let local = make_section_locality locality in
+ let local = make_section_locality atts.locality in
Arguments_renaming.rename_arguments local sr names
end;
@@ -1194,20 +1195,20 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
with UserError _ ->
Notation.find_delimiters_scope ?loc k)) scopes
in
- vernac_arguments_scope locality reference scopes
+ vernac_arguments_scope ~atts reference scopes
end;
if implicits_specified || clear_implicits_flag then
- vernac_declare_implicits locality reference implicits;
+ vernac_declare_implicits ~atts reference implicits;
if default_implicits_flag then
- vernac_declare_implicits locality reference [];
+ vernac_declare_implicits ~atts reference [];
if red_modifiers_specified then begin
match sr with
| ConstRef _ as c ->
Reductionops.ReductionBehaviour.set
- (make_section_locality locality) c
+ (make_section_locality atts.locality) c
(rargs, Option.default ~-1 nargs_for_red, red_flags)
| _ -> user_err
(strbrk "Modifiers of the behavior of the simpl tactic "++
@@ -1235,8 +1236,8 @@ let vernac_reserve bl =
Reserve.declare_reserved_type idl t)
in List.iter sb_decl bl
-let vernac_generalizable locality =
- let local = make_non_locality locality in
+let vernac_generalizable ~atts =
+ let local = make_non_locality atts.locality in
Implicit_quantifiers.declare_generalizable local
let _ =
@@ -1473,8 +1474,8 @@ let _ =
optread = Nativenorm.get_profiling_enabled;
optwrite = Nativenorm.set_profiling_enabled }
-let vernac_set_strategy locality l =
- let local = make_locality locality in
+let vernac_set_strategy ~atts l =
+ let local = make_locality atts.locality in
let glob_ref r =
match smart_global r with
| ConstRef sp -> EvalConstRef sp
@@ -1484,8 +1485,8 @@ let vernac_set_strategy locality l =
let l = List.map (fun (lev,ql) -> (lev,List.map glob_ref ql)) l in
Redexpr.set_strategy local l
-let vernac_set_opacity locality (v,l) =
- let local = make_non_locality locality in
+let vernac_set_opacity ~atts (v,l) =
+ let local = make_non_locality atts.locality in
let glob_ref r =
match smart_global r with
| ConstRef sp -> EvalConstRef sp
@@ -1495,18 +1496,18 @@ let vernac_set_opacity locality (v,l) =
let l = List.map glob_ref l in
Redexpr.set_strategy local [v,l]
-let vernac_set_option locality key = function
- | StringValue s -> set_string_option_value_gen locality key s
- | StringOptValue (Some s) -> set_string_option_value_gen locality key s
- | StringOptValue None -> unset_option_value_gen locality key
- | IntValue n -> set_int_option_value_gen locality key n
- | BoolValue b -> set_bool_option_value_gen locality key b
+let vernac_set_option ~atts key = function
+ | StringValue s -> set_string_option_value_gen atts.locality key s
+ | StringOptValue (Some s) -> set_string_option_value_gen atts.locality key s
+ | StringOptValue None -> unset_option_value_gen atts.locality key
+ | IntValue n -> set_int_option_value_gen atts.locality key n
+ | BoolValue b -> set_bool_option_value_gen atts.locality key b
-let vernac_set_append_option locality key s =
- set_string_option_append_value_gen locality key s
+let vernac_set_append_option ~atts key s =
+ set_string_option_append_value_gen atts.locality key s
-let vernac_unset_option locality key =
- unset_option_value_gen locality key
+let vernac_unset_option ~atts key =
+ unset_option_value_gen atts.locality key
let vernac_add_option key lv =
let f = function
@@ -1547,16 +1548,16 @@ let query_command_selector ?loc = function
| _ -> user_err ?loc ~hdr:"query_command_selector"
(str "Query commands only support the single numbered goal selector.")
-let vernac_check_may_eval ?loc redexp glopt rc =
- let glopt = query_command_selector ?loc glopt in
+let vernac_check_may_eval ~atts redexp glopt rc =
+ let glopt = query_command_selector ?loc:atts.loc glopt in
let (sigma, env) = get_current_context_of_args glopt in
let sigma', c = interp_open_constr env sigma rc in
let c = EConstr.Unsafe.to_constr c in
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 +1573,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 =
@@ -1582,8 +1583,8 @@ let vernac_check_may_eval ?loc redexp glopt rc =
in
Feedback.msg_notice (print_eval redfun env sigma' rc j)
-let vernac_declare_reduction locality s r =
- let local = make_locality locality in
+let vernac_declare_reduction ~atts s r =
+ let local = make_locality atts.locality in
declare_red_expr local s (snd (Hook.get f_interp_redexp (Global.env()) Evd.empty r))
(* The same but avoiding the current goal context if any *)
@@ -1609,9 +1610,10 @@ exception NoHyp
(* Printing "About" information of a hypothesis of the current goal.
We only print the type and a small statement to this comes from the
goal. Precondition: there must be at least one current goal. *)
-let print_about_hyp_globs ?loc ref_or_by_not glopt =
+let print_about_hyp_globs ?loc ref_or_by_not udecl glopt =
let open Context.Named.Declaration in
try
+ (* FIXME error on non None udecl if we find the hyp. *)
let glnumopt = query_command_selector ?loc glopt in
let gl,id =
match glnumopt,ref_or_by_not with
@@ -1634,10 +1636,12 @@ let print_about_hyp_globs ?loc ref_or_by_not glopt =
with (* fallback to globals *)
| NoHyp | Not_found ->
let sigma, env = Pfedit.get_current_context () in
- print_about env sigma ref_or_by_not
-
+ print_about env sigma ref_or_by_not udecl
-let vernac_print ?loc env sigma = let open Feedback in function
+let vernac_print ~atts env sigma =
+ let open Feedback in
+ let loc = atts.loc in
+ function
| PrintTables -> msg_notice (print_tables ())
| PrintFullContext-> msg_notice (print_full_context_typ env sigma)
| PrintSectionContext qid -> msg_notice (print_sec_context_typ env sigma qid)
@@ -1651,7 +1655,7 @@ let vernac_print ?loc env sigma = let open Feedback in function
| PrintMLLoadPath -> msg_notice (Mltop.print_ml_path ())
| PrintMLModules -> msg_notice (Mltop.print_ml_modules ())
| PrintDebugGC -> msg_notice (Mltop.print_gc ())
- | PrintName qid -> dump_global qid; msg_notice (print_name env sigma qid)
+ | PrintName (qid,udecl) -> dump_global qid; msg_notice (print_name env sigma qid udecl)
| PrintGraph -> msg_notice (Prettyp.print_graph())
| PrintClasses -> msg_notice (Prettyp.print_classes())
| PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses())
@@ -1681,8 +1685,8 @@ let vernac_print ?loc env sigma = let open Feedback in function
msg_notice (Notation.pr_scope (Constrextern.without_symbols (pr_lglob_constr_env env)) s)
| PrintVisibility s ->
msg_notice (Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s)
- | PrintAbout (ref_or_by_not,glnumopt) ->
- msg_notice (print_about_hyp_globs ?loc ref_or_by_not glnumopt)
+ | PrintAbout (ref_or_by_not,udecl,glnumopt) ->
+ msg_notice (print_about_hyp_globs ?loc ref_or_by_not udecl glnumopt)
| PrintImplicit qid ->
dump_global qid; msg_notice (print_impargs qid)
| PrintAssumptions (o,t,r) ->
@@ -1746,8 +1750,8 @@ let _ =
optread = (fun () -> !search_output_name_only);
optwrite = (:=) search_output_name_only }
-let vernac_search ?loc s gopt r =
- let gopt = query_command_selector ?loc gopt in
+let vernac_search ~atts s gopt r =
+ let gopt = query_command_selector ?loc:atts.loc gopt in
let r = interp_search_restriction r in
let env,gopt =
match gopt with | None ->
@@ -1914,7 +1918,8 @@ let vernac_load interp fname =
* is the outdated/deprecated "Local" attribute of some vernacular commands
* still parsed as the obsolete_locality grammar entry for retrocompatibility.
* loc is the Loc.t of the vernacular command being interpreted. *)
-let interp ?proof ?loc locality poly st c =
+let interp ?proof ~atts ~st c =
+ let open Vernacinterp in
vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac c);
match c with
(* The below vernac are candidates for removal from the main type
@@ -1953,31 +1958,33 @@ let interp ?proof ?loc locality poly st c =
| VernacLocal _ -> assert false
(* Syntax *)
- | VernacSyntaxExtension (infix, local,sl) ->
- vernac_syntax_extension locality local infix sl
+ | VernacSyntaxExtension (infix, sl) ->
+ vernac_syntax_extension atts infix sl
| VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
| VernacBindScope (sc,rl) -> vernac_bind_scope sc rl
- | VernacOpenCloseScope (local, s) -> vernac_open_close_scope locality local s
- | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope locality qid scl
- | VernacInfix (local,mv,qid,sc) -> vernac_infix locality local mv qid sc
- | VernacNotation (local,c,infpl,sc) ->
- vernac_notation locality local c infpl sc
+ | VernacOpenCloseScope (b, s) -> vernac_open_close_scope ~atts (b,s)
+ | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope ~atts qid scl
+ | VernacInfix (mv,qid,sc) -> vernac_infix ~atts mv qid sc
+ | VernacNotation (c,infpl,sc) ->
+ vernac_notation ~atts c infpl sc
| VernacNotationAddFormat(n,k,v) ->
Metasyntax.add_notation_extra_printing_rule n k v
(* Gallina *)
- | VernacDefinition (k,lid,d) -> vernac_definition locality poly k lid d
- | VernacStartTheoremProof (k,l) -> vernac_start_proof locality poly k l
+ | VernacDefinition ((discharge,kind),lid,d) ->
+ vernac_definition ~atts discharge kind lid d
+ | VernacStartTheoremProof (k,l) -> vernac_start_proof ~atts k l
| VernacEndProof e -> vernac_end_proof ?proof e
| VernacExactProof c -> vernac_exact_proof c
- | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl
- | VernacInductive (cum, priv,finite,l) -> vernac_inductive cum poly priv finite l
- | VernacFixpoint (local, l) -> vernac_fixpoint locality poly local l
- | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l
+ | VernacAssumption ((discharge,kind),nl,l) ->
+ vernac_assumption ~atts discharge kind l nl
+ | VernacInductive (cum, priv,finite,l) -> vernac_inductive ~atts cum priv finite l
+ | VernacFixpoint (discharge, l) -> vernac_fixpoint ~atts discharge l
+ | VernacCoFixpoint (discharge, l) -> vernac_cofixpoint ~atts discharge l
| VernacScheme l -> vernac_scheme l
| VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
- | VernacUniverse l -> vernac_universe loc poly l
- | VernacConstraint l -> vernac_constraint loc poly l
+ | VernacUniverse l -> vernac_universe ~atts l
+ | VernacConstraint l -> vernac_constraint ~atts l
(* Modules *)
| VernacDeclareModule (export,lid,bl,mtyo) ->
@@ -1998,15 +2005,15 @@ let interp ?proof ?loc locality poly st c =
| VernacRequire (from, export, qidl) -> vernac_require from export qidl
| VernacImport (export,qidl) -> vernac_import export qidl
| VernacCanonical qid -> vernac_canonical qid
- | VernacCoercion (local,r,s,t) -> vernac_coercion locality poly local r s t
- | VernacIdentityCoercion (local,(_,id),s,t) ->
- vernac_identity_coercion locality poly local id s t
+ | VernacCoercion (r,s,t) -> vernac_coercion ~atts r s t
+ | VernacIdentityCoercion ((_,id),s,t) ->
+ vernac_identity_coercion ~atts id s t
(* Type classes *)
| VernacInstance (abst, sup, inst, props, info) ->
- vernac_instance abst locality poly sup inst props info
- | VernacContext sup -> vernac_context poly sup
- | VernacDeclareInstances insts -> vernac_declare_instances locality insts
+ vernac_instance ~atts abst sup inst props info
+ | VernacContext sup -> vernac_context ~atts sup
+ | VernacDeclareInstances insts -> vernac_declare_instances ~atts insts
| VernacDeclareClass id -> vernac_declare_class id
(* Solving *)
@@ -2016,7 +2023,7 @@ let interp ?proof ?loc locality poly st c =
| VernacAddLoadPath (isrec,s,alias) -> vernac_add_loadpath isrec s alias
| VernacRemoveLoadPath s -> vernac_remove_loadpath s
| VernacAddMLPath (isrec,s) -> vernac_add_ml_path isrec s
- | VernacDeclareMLModule l -> vernac_declare_ml_module locality l
+ | VernacDeclareMLModule l -> vernac_declare_ml_module ~atts l
| VernacChdir s -> vernac_chdir s
(* State management *)
@@ -2024,40 +2031,40 @@ let interp ?proof ?loc locality poly st c =
| VernacRestoreState s -> vernac_restore_state s
(* Commands *)
- | VernacCreateHintDb (dbname,b) -> vernac_create_hintdb locality dbname b
- | VernacRemoveHints (dbnames,ids) -> vernac_remove_hints locality dbnames ids
- | VernacHints (local,dbnames,hints) ->
- vernac_hints locality poly local dbnames hints
- | VernacSyntacticDefinition (id,c,local,b) ->
- vernac_syntactic_definition locality id c local b
+ | VernacCreateHintDb (dbname,b) -> vernac_create_hintdb ~atts dbname b
+ | VernacRemoveHints (dbnames,ids) -> vernac_remove_hints ~atts dbnames ids
+ | VernacHints (dbnames,hints) ->
+ vernac_hints ~atts dbnames hints
+ | VernacSyntacticDefinition (id,c,b) ->
+ vernac_syntactic_definition ~atts id c b
| VernacDeclareImplicits (qid,l) ->
- vernac_declare_implicits locality qid l
+ vernac_declare_implicits ~atts qid l
| VernacArguments (qid, args, more_implicits, nargs, flags) ->
- vernac_arguments locality qid args more_implicits nargs flags
+ vernac_arguments ~atts qid args more_implicits nargs flags
| VernacReserve bl -> vernac_reserve bl
- | VernacGeneralizable gen -> vernac_generalizable locality gen
- | VernacSetOpacity qidl -> vernac_set_opacity locality qidl
- | VernacSetStrategy l -> vernac_set_strategy locality l
- | VernacSetOption (key,v) -> vernac_set_option locality key v
- | VernacSetAppendOption (key,v) -> vernac_set_append_option locality key v
- | VernacUnsetOption key -> vernac_unset_option locality key
+ | VernacGeneralizable gen -> vernac_generalizable ~atts gen
+ | VernacSetOpacity qidl -> vernac_set_opacity ~atts qidl
+ | VernacSetStrategy l -> vernac_set_strategy ~atts l
+ | VernacSetOption (key,v) -> vernac_set_option ~atts key v
+ | VernacSetAppendOption (key,v) -> vernac_set_append_option ~atts key v
+ | VernacUnsetOption key -> vernac_unset_option ~atts key
| VernacRemoveOption (key,v) -> vernac_remove_option key v
| VernacAddOption (key,v) -> vernac_add_option key v
| VernacMemOption (key,v) -> vernac_mem_option key v
| VernacPrintOption key -> vernac_print_option key
- | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval ?loc r g c
- | VernacDeclareReduction (s,r) -> vernac_declare_reduction locality s r
+ | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval ~atts r g c
+ | VernacDeclareReduction (s,r) -> vernac_declare_reduction ~atts s r
| VernacGlobalCheck c -> vernac_global_check c
| VernacPrint p ->
let sigma, env = Pfedit.get_current_context () in
- vernac_print ?loc env sigma p
- | VernacSearch (s,g,r) -> vernac_search ?loc s g r
+ vernac_print ~atts env sigma p
+ | VernacSearch (s,g,r) -> vernac_search ~atts s g r
| VernacLocate l -> vernac_locate l
| VernacRegister (id, r) -> vernac_register id r
| VernacComments l -> Flags.if_verbose Feedback.msg_info (str "Comments ok\n")
(* Proof management *)
- | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t)]
+ | VernacGoal t -> vernac_start_proof ~atts Theorem [None,([],t)]
| VernacFocus n -> vernac_focus n
| VernacUnfocus -> vernac_unfocus ()
| VernacUnfocused -> vernac_unfocused ()
@@ -2070,7 +2077,7 @@ let interp ?proof ?loc locality poly st c =
let using = Option.append using (Proof_using.get_default_proof_using ()) in
let tacs = if Option.is_empty tac then "tac:no" else "tac:yes" in
let usings = if Option.is_empty using then "using:no" else "using:yes" in
- Aux_file.record_in_aux_at ?loc "VernacProof" (tacs^" "^usings);
+ Aux_file.record_in_aux_at ?loc:atts.loc "VernacProof" (tacs^" "^usings);
Option.iter vernac_set_end_tac tac;
Option.iter vernac_set_used_variables using
| VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"]
@@ -2078,7 +2085,7 @@ let interp ?proof ?loc locality poly st c =
(* Extensions *)
| VernacExtend (opn,args) ->
(* XXX: Here we are returning the state! :) *)
- let _st : Vernacstate.t = Vernacinterp.call ?locality ?loc (opn,args) ~st in
+ let _st : Vernacstate.t = Vernacinterp.call ~atts opn args ~st in
()
(* Vernaculars that take a locality flag *)
@@ -2110,7 +2117,7 @@ let check_vernac_supports_polymorphism c p =
| None, _ -> ()
| Some _, (
VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _
- | VernacAssumption _ | VernacInductive _
+ | VernacAssumption _ | VernacInductive _
| VernacStartTheoremProof _
| VernacCoercion _ | VernacIdentityCoercion _
| VernacInstance _ | VernacDeclareInstances _
@@ -2119,7 +2126,7 @@ let check_vernac_supports_polymorphism c p =
| Some _, _ -> user_err Pp.(str "This command does not support Polymorphism")
let enforce_polymorphism = function
- | None -> Flags.is_universe_polymorphism ()
+ | None -> Flags.is_universe_polymorphism ()
| Some b -> Flags.make_polymorphic_flag b; b
(** A global default timeout, controlled by option "Set Default Timeout n".
@@ -2187,42 +2194,57 @@ let with_fail st b f =
| _ -> assert false
end
-let interp ?(verbosely=true) ?proof st (loc,c) =
+let interp ?(verbosely=true) ?proof ~st (loc,c) =
let orig_program_mode = Flags.is_program_mode () in
- let rec aux ?locality ?polymorphism isprogcmd = function
-
- | VernacProgram c when not isprogcmd -> aux ?locality ?polymorphism true c
- | VernacProgram _ -> user_err Pp.(str "Program mode specified twice")
- | VernacLocal (b, c) when Option.is_empty locality ->
- aux ~locality:b ?polymorphism isprogcmd c
- | VernacPolymorphic (b, c) when polymorphism = None ->
- aux ?locality ~polymorphism:b isprogcmd c
- | VernacPolymorphic (b, c) -> user_err Pp.(str "Polymorphism specified twice")
- | VernacLocal _ -> user_err Pp.(str "Locality specified twice")
+ let rec aux ?polymorphism ~atts isprogcmd = function
+
+ | VernacProgram c when not isprogcmd ->
+ aux ?polymorphism ~atts true c
+
+ | VernacProgram _ ->
+ user_err Pp.(str "Program mode specified twice")
+
+ | VernacPolymorphic (b, c) when polymorphism = None ->
+ aux ~polymorphism:b ~atts:atts isprogcmd c
+
+ | VernacPolymorphic (b, c) ->
+ user_err Pp.(str "Polymorphism specified twice")
+
+ | VernacLocal (b, c) when Option.is_empty atts.locality ->
+ aux ?polymorphism ~atts:{atts with locality = Some b} isprogcmd c
+
+ | VernacLocal _ ->
+ user_err Pp.(str "Locality specified twice")
+
| VernacFail v ->
- with_fail st true (fun () -> aux ?locality ?polymorphism isprogcmd v)
+ with_fail st true (fun () -> aux ?polymorphism ~atts isprogcmd v)
+
| VernacTimeout (n,v) ->
- current_timeout := Some n;
- aux ?locality ?polymorphism isprogcmd v
+ current_timeout := Some n;
+ aux ?polymorphism ~atts isprogcmd v
+
| VernacRedirect (s, (_,v)) ->
- Topfmt.with_output_to_file s (aux ?locality ?polymorphism isprogcmd) v
+ Topfmt.with_output_to_file s (aux ?polymorphism ~atts isprogcmd) v
+
| VernacTime (_,v) ->
- System.with_time !Flags.time
- (aux ?locality ?polymorphism isprogcmd) v;
- | VernacLoad (_,fname) -> vernac_load (aux false) fname
- | c ->
- check_vernac_supports_locality c locality;
- check_vernac_supports_polymorphism c polymorphism;
- let poly = enforce_polymorphism polymorphism in
- Obligations.set_program_mode isprogcmd;
- try
- vernac_timeout begin fun () ->
+ System.with_time !Flags.time (aux ?polymorphism ~atts isprogcmd) v;
+
+ | VernacLoad (_,fname) -> vernac_load (aux ?polymorphism ~atts false) fname
+
+ | c ->
+ check_vernac_supports_locality c atts.locality;
+ check_vernac_supports_polymorphism c polymorphism;
+ let polymorphic = enforce_polymorphism polymorphism in
+ Obligations.set_program_mode isprogcmd;
+ try
+ vernac_timeout begin fun () ->
+ let atts = { atts with polymorphic } in
if verbosely
- then Flags.verbosely (interp ?proof ?loc locality poly st) c
- else Flags.silently (interp ?proof ?loc locality poly st) c;
+ then Flags.verbosely (interp ?proof ~atts ~st) c
+ else Flags.silently (interp ?proof ~atts ~st) c;
if orig_program_mode || not !Flags.program_mode || isprogcmd then
Flags.program_mode := orig_program_mode;
- ignore (Flags.use_polymorphic_flag ())
+ ignore (Flags.use_polymorphic_flag ())
end
with
| reraise when
@@ -2237,12 +2259,19 @@ let interp ?(verbosely=true) ?proof st (loc,c) =
ignore (Flags.use_polymorphic_flag ());
iraise e
in
- if verbosely then Flags.verbosely (aux false) c
- else aux false c
+ let atts = { loc; locality = None; polymorphic = false; } in
+ if verbosely
+ then Flags.verbosely (aux ~atts orig_program_mode) c
+ else aux ~atts orig_program_mode c
(* XXX: There is a bug here in case of an exception, see @gares
comments on the PR *)
-let interp ?verbosely ?proof st cmd =
+let interp ?verbosely ?proof ~st cmd =
Vernacstate.unfreeze_interp_state st;
- interp ?verbosely ?proof st cmd;
- Vernacstate.freeze_interp_state `No
+ try
+ interp ?verbosely ?proof ~st cmd;
+ Vernacstate.freeze_interp_state `No
+ with exn ->
+ let exn = CErrors.push exn in
+ Vernacstate.invalidate_cache ();
+ iraise exn
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 67001bc24e..a559912a09 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -18,7 +18,7 @@ val vernac_require :
val interp :
?verbosely:bool ->
?proof:Proof_global.closed_proof ->
- Vernacstate.t -> Vernacexpr.vernac_expr Loc.located -> Vernacstate.t
+ st:Vernacstate.t -> Vernacexpr.vernac_expr Loc.located -> Vernacstate.t
(** Prepare a "match" template for a given inductive type.
For each branch of the match, we list the constructor name
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 47dec19588..c0b93c1638 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -15,17 +15,17 @@ type deprecation = bool
type atts = {
loc : Loc.t option;
locality : bool option;
+ polymorphic : bool;
}
-type vernac_command =
- Genarg.raw_generic_argument list ->
- atts:atts -> st:Vernacstate.t ->
- Vernacstate.t
+type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
+
+type plugin_args = Genarg.raw_generic_argument list
(* Table of vernac entries *)
let vernac_tab =
(Hashtbl.create 211 :
- (Vernacexpr.extend_name, deprecation * vernac_command) Hashtbl.t)
+ (Vernacexpr.extend_name, deprecation * plugin_args vernac_command) Hashtbl.t)
let vinterp_add depr s f =
try
@@ -58,7 +58,7 @@ let warn_deprecated_command =
(* Interpretation of a vernac command *)
-let call ?locality ?loc (opn,converted_args) =
+let call opn converted_args ~atts ~st =
let phase = ref "Looking up command" in
try
let depr, callback = vinterp_map opn in
@@ -74,8 +74,7 @@ let call ?locality ?loc (opn,converted_args) =
phase := "Checking arguments";
let hunk = callback converted_args in
phase := "Executing command";
- let atts = { loc; locality } in
- hunk ~atts
+ hunk ~atts ~st
with
| Drop -> raise Drop
| reraise ->
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index 602ccba157..ab3d4bfc52 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -13,19 +13,15 @@ type deprecation = bool
type atts = {
loc : Loc.t option;
locality : bool option;
+ polymorphic : bool;
}
-type vernac_command =
- Genarg.raw_generic_argument list ->
- atts:atts -> st:Vernacstate.t ->
- Vernacstate.t
+type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
-val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit
-
-val overwriting_vinterp_add : Vernacexpr.extend_name -> vernac_command -> unit
+type plugin_args = Genarg.raw_generic_argument list
val vinterp_init : unit -> unit
+val vinterp_add : deprecation -> Vernacexpr.extend_name -> plugin_args vernac_command -> unit
+val overwriting_vinterp_add : Vernacexpr.extend_name -> plugin_args vernac_command -> unit
-val call : ?locality:bool -> ?loc:Loc.t ->
- Vernacexpr.extend_name * Genarg.raw_generic_argument list ->
- st:Vernacstate.t -> Vernacstate.t
+val call : Vernacexpr.extend_name -> plugin_args -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index eb1359d52b..4980333b5d 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -8,22 +8,34 @@
type t = {
system : States.state; (* summary + libstack *)
- proof : Proof_global.state; (* proof state *)
+ proof : Proof_global.t; (* proof state *)
shallow : bool (* is the state trimmed down (libstack) *)
}
-let s_cache = ref (States.freeze ~marshallable:`No)
-let s_proof = ref (Proof_global.freeze ~marshallable:`No)
+let s_cache = ref None
+let s_proof = ref None
let invalidate_cache () =
- s_cache := Obj.magic 0;
- s_proof := Obj.magic 0
+ s_cache := None;
+ s_proof := None
+
+let update_cache rf v =
+ rf := Some v; v
+
+let do_if_not_cached rf f v =
+ match !rf with
+ | None ->
+ rf := Some v; f v
+ | Some vc when vc != v ->
+ rf := Some v; f v
+ | Some _ ->
+ ()
let freeze_interp_state marshallable =
- { system = (s_cache := States.freeze ~marshallable; !s_cache);
- proof = (s_proof := Proof_global.freeze ~marshallable; !s_proof);
+ { system = update_cache s_cache (States.freeze ~marshallable);
+ proof = update_cache s_proof (Proof_global.freeze ~marshallable);
shallow = marshallable = `Shallow }
let unfreeze_interp_state { system; proof } =
- if (!s_cache != system) then (s_cache := system; States.unfreeze system);
- if (!s_proof != proof) then (s_proof := proof; Proof_global.unfreeze proof)
+ do_if_not_cached s_cache States.unfreeze system;
+ do_if_not_cached s_proof Proof_global.unfreeze proof
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index bcfa49aa38..3ed27ddb7a 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -8,7 +8,7 @@
type t = {
system : States.state; (* summary + libstack *)
- proof : Proof_global.state; (* proof state *)
+ proof : Proof_global.t; (* proof state *)
shallow : bool (* is the state trimmed down (libstack) *)
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 17:41:16 +0000