aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/class.ml6
-rw-r--r--vernac/classes.ml20
-rw-r--r--vernac/comAssumption.ml20
-rw-r--r--vernac/comAssumption.mli2
-rw-r--r--vernac/comDefinition.ml42
-rw-r--r--vernac/comInductive.ml13
-rw-r--r--vernac/comProgramFixpoint.ml4
-rw-r--r--vernac/declareDef.ml14
-rw-r--r--vernac/declareDef.mli28
-rw-r--r--vernac/explainErr.ml2
-rw-r--r--vernac/g_vernac.mlg18
-rw-r--r--vernac/himsg.ml43
-rw-r--r--vernac/himsg.mli2
-rw-r--r--vernac/indschemes.ml2
-rw-r--r--vernac/lemmas.ml76
-rw-r--r--vernac/lemmas.mli38
-rw-r--r--vernac/obligations.ml72
-rw-r--r--vernac/obligations.mli29
-rw-r--r--vernac/pvernac.ml2
-rw-r--r--vernac/pvernac.mli4
-rw-r--r--vernac/record.ml50
-rw-r--r--vernac/record.mli2
-rw-r--r--vernac/vernacentries.ml40
-rw-r--r--vernac/vernacentries.mli4
24 files changed, 241 insertions, 292 deletions
diff --git a/vernac/class.ml b/vernac/class.ml
index 8374a5c84f..a6b3242cae 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -215,7 +215,7 @@ let build_id_coercion idf_opt source poly =
Id.of_string ("Id_"^(ident_key_of_class source)^"_"^
(ident_key_of_class cl))
in
- let univs = Evd.const_univ_entry ~poly sigma in
+ let univs = Evd.univ_entry ~poly sigma in
let constr_entry = (* Cast is necessary to express [val_f] is identity *)
DefinitionEntry
(definition_entry ~types:typ_f ~univs
@@ -302,7 +302,7 @@ let try_add_new_identity_coercion id ~local poly ~source ~target =
let try_add_new_coercion_with_source ref ~local poly ~source =
try_add_new_coercion_core ref ~local poly (Some source) None false
-let add_coercion_hook poly local ref =
+let add_coercion_hook poly _uctx _trans local ref =
let local = match local with
| Discharge
| Local -> true
@@ -314,7 +314,7 @@ let add_coercion_hook poly local ref =
let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly)
-let add_subclass_hook poly local ref =
+let add_subclass_hook poly _uctx _trans local ref =
let stre = match local with
| Local -> true
| Global -> false
diff --git a/vernac/classes.ml b/vernac/classes.ml
index ea434dbc4f..263ebf5f5a 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -106,7 +106,7 @@ let id_of_class cl =
| _ -> assert false
let instance_hook k info global imps ?hook cst =
- Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps;
+ Impargs.maybe_declare_manual_implicits false cst imps;
let info = intern_info info in
Typeclasses.declare_instance (Some info) (not global) cst;
(match hook with Some h -> h cst | None -> ())
@@ -149,7 +149,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
if program_mode then
let hook _ _ vis gr =
let cst = match gr with ConstRef kn -> kn | _ -> assert false in
- Impargs.declare_manual_implicits false gr ~enriching:false [imps];
+ Impargs.declare_manual_implicits false gr [imps];
let pri = intern_info pri in
Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst)
in
@@ -161,10 +161,10 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
in obls, Some constr, typ
| None -> [||], None, termtype
in
- let univ_hook = Obligations.mk_univ_hook hook in
+ let hook = Lemmas.mk_hook hook in
let ctx = Evd.evar_universe_context sigma in
ignore (Obligations.add_definition id ?term:constr
- ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~univ_hook obls)
+ ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls)
else
Flags.silently (fun () ->
(* spiwack: it is hard to reorder the actions to do
@@ -175,7 +175,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
let sigma = Evd.reset_future_goals sigma in
Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype)
~hook:(Lemmas.mk_hook
- (fun _ -> instance_hook k pri global imps ?hook));
+ (fun _ _ _ -> instance_hook k pri global imps ?hook));
(* spiwack: I don't know what to do with the status here. *)
if not (Option.is_empty term) then
let init_refine =
@@ -374,7 +374,7 @@ let context poly l =
let univs =
match ctx with
| [] -> assert false
- | [_] -> Evd.const_univ_entry ~poly sigma
+ | [_] -> Evd.univ_entry ~poly sigma
| _::_::_ ->
if Lib.sections_are_opened ()
then
@@ -384,19 +384,19 @@ let context poly l =
begin
let uctx = Evd.universe_context_set sigma in
Declare.declare_universe_context poly uctx;
- if poly then Polymorphic_const_entry ([||], Univ.UContext.empty)
- else Monomorphic_const_entry Univ.ContextSet.empty
+ if poly then Polymorphic_entry ([||], Univ.UContext.empty)
+ else Monomorphic_entry Univ.ContextSet.empty
end
else if poly then
(* Multiple polymorphic axioms: they are all polymorphic the same way. *)
- Evd.const_univ_entry ~poly sigma
+ Evd.univ_entry ~poly sigma
else
(* Multiple monomorphic axioms: declare universes separately
to avoid redeclaring them. *)
begin
let uctx = Evd.universe_context_set sigma in
Declare.declare_universe_context poly uctx;
- Monomorphic_const_entry Univ.ContextSet.empty
+ Monomorphic_entry Univ.ContextSet.empty
end
in
let fn status (id, b, t) =
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 73d0be04df..35d8be5c56 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -8,7 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Pp
open CErrors
open Util
open Vars
@@ -46,18 +45,19 @@ let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ide
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
+ | Monomorphic_entry ctx -> ctx
+ | Polymorphic_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
let () =
if not !Flags.quiet && Proof_global.there_are_pending_proofs () then
- Feedback.msg_info (str"Variable" ++ spc () ++ Id.print ident ++
+ Feedback.msg_info Pp.(str"Variable" ++ spc () ++ Id.print ident ++
strbrk " is not visible from current goals")
in
let r = VarRef ident in
+ let () = maybe_declare_manual_implicits true r imps in
let () = Typeclasses.declare_instance None true r in
let () = if is_coe then Class.try_add_new_coercion r ~local:true false in
(r,Univ.Instance.empty,true)
@@ -79,8 +79,8 @@ match local with
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 = match ctx with
- | Polymorphic_const_entry (_, ctx) -> Univ.UContext.instance ctx
- | Monomorphic_const_entry _ -> Univ.Instance.empty
+ | Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx
+ | Monomorphic_entry _ -> Univ.Instance.empty
in
(gr,inst,Lib.is_modtype_strict ())
@@ -90,10 +90,10 @@ let interp_assumption ~program_mode sigma env impls c =
(* 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
+ let empty_uctx = Monomorphic_entry Univ.ContextSet.empty in
function
- | Polymorphic_const_entry _ as uctx -> uctx
- | Monomorphic_const_entry _ -> empty_uctx
+ | Polymorphic_entry _ as uctx -> uctx
+ | Monomorphic_entry _ -> empty_uctx
let declare_assumptions idl is_coe k (c,uctx) pl imps nl =
let refs, status, _ =
@@ -203,4 +203,4 @@ let do_primitive id prim typopt =
}
in
let _kn = declare_constant id.CAst.v (PrimitiveEntry entry,IsPrimitive) in
- register_message id.CAst.v
+ Flags.if_verbose Feedback.msg_info Pp.(Id.print id.CAst.v ++ str " is declared")
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 385ec33bea..2b794b001a 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -29,7 +29,7 @@ val do_assumptions : program_mode:bool -> locality * polymorphic * assumption_ob
(** 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 in_constant_universes_entry ->
+ types in_universes_entry ->
UnivNames.universe_binders -> Impargs.manual_implicits ->
bool (** implicit *) -> Declaremods.inline -> variable CAst.t ->
GlobRef.t * Univ.Instance.t * bool
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 5e74114a86..28773a3965 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -35,7 +35,7 @@ let check_imps ~impsty ~impsbody =
try
List.for_all (fun (key, (va:bool*bool*bool)) ->
(* Pervasives.(=) is OK for this type *)
- Pervasives.(=) (List.assoc_f Impargs.explicitation_eq key impsty) va)
+ Pervasives.(=) (List.assoc_f Constrexpr_ops.explicitation_eq key impsty) va)
impsbody
with Not_found -> false
in
@@ -94,22 +94,24 @@ let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
let (ce, evd, univdecl, imps as def) =
interp_definition ~program_mode univdecl bl (pi2 k) red_option c ctypopt
in
- if program_mode then
- let env = Global.env () in
- let (c,ctx), sideff = Future.force ce.const_entry_body in
- assert(Safe_typing.empty_private_constants = sideff);
- assert(Univ.ContextSet.is_empty ctx);
- let typ = match ce.const_entry_type with
- | Some t -> t
- | None -> EConstr.to_constr ~abort_on_undefined_evars:false evd (Retyping.get_type_of env evd (EConstr.of_constr c))
- in
- Obligations.check_evars env evd;
- let obls, _, c, cty =
- Obligations.eterm_obligations env ident evd 0 c typ
- in
- let ctx = Evd.evar_universe_context evd in
- let univ_hook = Obligations.mk_univ_hook (fun _ _ l r -> Lemmas.call_hook ?hook l r) in
- ignore(Obligations.add_definition
- ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~univ_hook obls)
- else let ce = check_definition ~program_mode def in
- ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps ?hook)
+ if program_mode then
+ let env = Global.env () in
+ let (c,ctx), sideff = Future.force ce.const_entry_body in
+ assert(Safe_typing.empty_private_constants = sideff);
+ assert(Univ.ContextSet.is_empty ctx);
+ let typ = match ce.const_entry_type with
+ | Some t -> t
+ | None -> EConstr.to_constr ~abort_on_undefined_evars:false evd (Retyping.get_type_of env evd (EConstr.of_constr c))
+ in
+ Obligations.check_evars env evd;
+ let obls, _, c, cty =
+ Obligations.eterm_obligations env ident evd 0 c typ
+ in
+ let ctx = Evd.evar_universe_context evd in
+ ignore(Obligations.add_definition
+ ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ?hook obls)
+ else
+ let ce = check_definition ~program_mode def in
+ let uctx = Evd.evar_universe_context evd in
+ let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
+ ignore(DeclareDef.declare_definition ident k ?hook_data ce (Evd.universe_binders evd) imps )
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 68ad276113..9bbfb8eec6 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -457,15 +457,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
indimpls, List.map (fun impls ->
userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors
in
- let univs =
- match uctx with
- | Polymorphic_const_entry (nas, uctx) ->
- if cum then
- Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context uctx)
- else Polymorphic_ind_entry (nas, uctx)
- | Monomorphic_const_entry uctx ->
- Monomorphic_ind_entry uctx
- in
+ let variance = if poly && cum then Some (InferCumulativity.dummy_variance uctx) else None in
(* Build the mutual inductive entry *)
let mind_ent =
{ mind_entry_params = ctx_params;
@@ -473,7 +465,8 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
mind_entry_finite = finite;
mind_entry_inds = entries;
mind_entry_private = if prv then Some false else None;
- mind_entry_universes = univs;
+ mind_entry_universes = uctx;
+ mind_entry_variance = variance;
}
in
(if poly && cum then
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index a30313d37c..cc9c83bd17 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -227,7 +227,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
in hook, recname, typ
in
(* XXX: Capturing sigma here... bad bad *)
- let univ_hook = Obligations.mk_univ_hook (hook sigma) in
+ let hook = Lemmas.mk_hook (hook sigma) in
(* XXX: Grounding non-ground terms here... bad bad *)
let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in
let fullctyp = EConstr.to_constr sigma typ in
@@ -237,7 +237,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
in
let ctx = Evd.evar_universe_context sigma in
ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl
- evars_typ ctx evars ~univ_hook)
+ evars_typ ctx evars ~hook)
let out_def = function
| Some def -> def
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 361ed1a737..7dcd098183 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -33,7 +33,7 @@ let get_locality id ~kind = function
| Local -> true
| Global -> false
-let declare_definition ident (local, p, k) ?hook ce pl imps =
+let declare_definition ident (local, p, k) ?hook_data ce pl imps =
let fix_exn = Future.fix_exn_of ce.const_entry_body in
let gr = match local with
| Discharge when Lib.sections_are_opened () ->
@@ -49,11 +49,17 @@ let declare_definition ident (local, p, k) ?hook ce pl imps =
in
let () = maybe_declare_manual_implicits false gr imps in
let () = definition_message ident in
- Lemmas.call_hook ~fix_exn ?hook local gr; gr
+ begin
+ match hook_data with
+ | None -> ()
+ | Some (hook, uctx, extra_defs) ->
+ Lemmas.call_hook ~fix_exn ~hook uctx extra_defs local gr
+ end;
+ gr
-let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
+let declare_fix ?(opaque = false) ?hook_data (_,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
+ declare_definition f kind ?hook_data ce pl imps
let check_definition_evars ~allow_evars sigma =
let env = Global.env () in
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 1e3644c371..3f95ec7107 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -13,16 +13,26 @@ open Decl_kinds
val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool
-val declare_definition : Id.t -> definition_kind ->
- ?hook:Lemmas.declaration_hook ->
- Safe_typing.private_constants Entries.definition_entry -> UnivNames.universe_binders -> Impargs.manual_implicits ->
- GlobRef.t
+val declare_definition
+ : Id.t
+ -> definition_kind
+ -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
+ -> Safe_typing.private_constants Entries.definition_entry
+ -> UnivNames.universe_binders
+ -> Impargs.manual_implicits
+ -> GlobRef.t
-val declare_fix : ?opaque:bool -> definition_kind ->
- UnivNames.universe_binders -> Entries.constant_universes_entry ->
- Id.t -> Safe_typing.private_constants Entries.proof_output ->
- Constr.types -> Impargs.manual_implicits ->
- GlobRef.t
+val declare_fix
+ : ?opaque:bool
+ -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
+ -> definition_kind
+ -> UnivNames.universe_binders
+ -> Entries.universes_entry
+ -> Id.t
+ -> Safe_typing.private_constants Entries.proof_output
+ -> Constr.types
+ -> Impargs.manual_implicits
+ -> GlobRef.t
val prepare_definition : allow_evars:bool ->
?opaque:bool -> ?inline:bool -> poly:bool ->
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 42b313f200..06428b53f2 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -58,7 +58,7 @@ let process_vernac_interp_error exn = match fst exn with
mt() in
wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".")
| TypeError(ctx,te) ->
- let te = Himsg.map_ptype_error EConstr.of_constr te in
+ let te = map_ptype_error EConstr.of_constr te in
wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te)
| PretypeError(ctx,sigma,te) ->
wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 0664e18130..42bee25da3 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -693,18 +693,20 @@ GRAMMAR EXTEND Gram
LIST1 [ v=strategy_level; "["; q=LIST1 smart_global; "]" -> { (v,q) } ] ->
{ VernacSetStrategy l }
(* Canonical structure *)
- | IDENT "Canonical"; IDENT "Structure"; qid = global ->
- { VernacCanonical CAst.(make ~loc @@ AN qid) }
- | IDENT "Canonical"; IDENT "Structure"; ntn = by_notation ->
+ | IDENT "Canonical"; OPT [ IDENT "Structure" -> {()} ]; qid = global; ud = OPT [ u = OPT univ_decl; d = def_body -> { (u,d) } ] ->
+ { match ud with
+ | None ->
+ VernacCanonical CAst.(make ~loc @@ AN qid)
+ | Some (u,d) ->
+ let s = coerce_reference_to_id qid in
+ VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),u),d) }
+ | IDENT "Canonical"; OPT [ IDENT "Structure" -> {()} ]; ntn = by_notation ->
{ VernacCanonical CAst.(make ~loc @@ ByNotation ntn) }
- | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body ->
- { let s = coerce_reference_to_id qid in
- VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),None),d) }
(* Coercions *)
- | IDENT "Coercion"; qid = global; d = def_body ->
+ | IDENT "Coercion"; qid = global; u = OPT univ_decl; d = def_body ->
{ let s = coerce_reference_to_id qid in
- VernacDefinition ((NoDischarge,Coercion),((CAst.make (Name s)),None),d) }
+ VernacDefinition ((NoDischarge,Coercion),((CAst.make (Name s)),u),d) }
| IDENT "Identity"; IDENT "Coercion"; f = identref; ":";
s = class_rawexpr; ">->"; t = class_rawexpr ->
{ VernacIdentityCoercion (f, s, t) }
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index f78b43e2fa..9dd321be51 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -923,6 +923,8 @@ let explain_not_match_error = function
str "but expected" ++ spc() ++ h 0 (pr_auctx expect) ++
(if not (Int.equal (AUContext.size got) (AUContext.size expect)) then mt() else
fnl() ++ str "(incompatible constraints)")
+ | IncompatibleVariance ->
+ str "incompatible variance information"
let explain_signature_mismatch l spec why =
str "Signature components for label " ++ Label.print l ++
@@ -1297,45 +1299,8 @@ let explain_pattern_matching_error env sigma = function
| CannotInferPredicate typs ->
explain_cannot_infer_predicate env sigma typs
-let map_pguard_error f = function
-| NotEnoughAbstractionInFixBody -> NotEnoughAbstractionInFixBody
-| RecursionNotOnInductiveType c -> RecursionNotOnInductiveType (f c)
-| RecursionOnIllegalTerm (n, (env, c), l1, l2) -> RecursionOnIllegalTerm (n, (env, f c), l1, l2)
-| NotEnoughArgumentsForFixCall n -> NotEnoughArgumentsForFixCall n
-| CodomainNotInductiveType c -> CodomainNotInductiveType (f c)
-| NestedRecursiveOccurrences -> NestedRecursiveOccurrences
-| UnguardedRecursiveCall c -> UnguardedRecursiveCall (f c)
-| RecCallInTypeOfAbstraction c -> RecCallInTypeOfAbstraction (f c)
-| RecCallInNonRecArgOfConstructor c -> RecCallInNonRecArgOfConstructor (f c)
-| RecCallInTypeOfDef c -> RecCallInTypeOfDef (f c)
-| RecCallInCaseFun c -> RecCallInCaseFun (f c)
-| RecCallInCaseArg c -> RecCallInCaseArg (f c)
-| RecCallInCasePred c -> RecCallInCasePred (f c)
-| NotGuardedForm c -> NotGuardedForm (f c)
-| ReturnPredicateNotCoInductive c -> ReturnPredicateNotCoInductive (f c)
-
-let map_ptype_error f = function
-| UnboundRel n -> UnboundRel n
-| UnboundVar id -> UnboundVar id
-| NotAType j -> NotAType (on_judgment f j)
-| BadAssumption j -> BadAssumption (on_judgment f j)
-| ReferenceVariables (id, c) -> ReferenceVariables (id, f c)
-| ElimArity (pi, dl, c, j, ar) -> ElimArity (pi, dl, f c, on_judgment f j, ar)
-| CaseNotInductive j -> CaseNotInductive (on_judgment f j)
-| WrongCaseInfo (pi, ci) -> WrongCaseInfo (pi, ci)
-| NumberBranches (j, n) -> NumberBranches (on_judgment f j, n)
-| IllFormedBranch (c, pc, t1, t2) -> IllFormedBranch (f c, pc, f t1, f t2)
-| Generalization ((na, t), j) -> Generalization ((na, f t), on_judgment f j)
-| ActualType (j, t) -> ActualType (on_judgment f j, f t)
-| CantApplyBadType ((n, c1, c2), j, vj) ->
- CantApplyBadType ((n, f c1, f c2), on_judgment f j, Array.map (on_judgment f) vj)
-| CantApplyNonFunctional (j, jv) -> CantApplyNonFunctional (on_judgment f j, Array.map (on_judgment f) jv)
-| IllFormedRecBody (ge, na, n, env, jv) ->
- IllFormedRecBody (map_pguard_error f ge, na, n, env, Array.map (on_judgment f) jv)
-| IllTypedRecBody (n, na, jv, t) ->
- IllTypedRecBody (n, na, Array.map (on_judgment f) jv, Array.map f t)
-| UnsatisfiedConstraints g -> UnsatisfiedConstraints g
-| UndeclaredUniverse l -> UndeclaredUniverse l
+let map_pguard_error = map_pguard_error
+let map_ptype_error = map_ptype_error
let explain_reduction_tactic_error = function
| Tacred.InvalidAbstraction (env,sigma,c,(env',e)) ->
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index 986906d303..f22354cdbf 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -44,6 +44,8 @@ val explain_module_internalization_error :
Modintern.module_internalization_error -> Pp.t
val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
+[@@ocaml.deprecated "Use [Type_errors.map_pguard_error]."]
val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error
+[@@ocaml.deprecated "Use [Type_errors.map_ptype_error]."]
val explain_prim_token_notation_error : string -> env -> Evd.evar_map -> Notation.prim_token_notation_error -> Pp.t
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index d29f66f81f..caafd6ac2f 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -103,7 +103,7 @@ let () =
let define ~poly id internal sigma c t =
let f = declare_constant ~internal in
- let univs = Evd.const_univ_entry ~poly sigma in
+ let univs = Evd.univ_entry ~poly sigma in
let kn = f id
(DefinitionEntry
{ const_entry_body = c;
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 4635883dc2..77f125e878 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -34,10 +34,13 @@ open Impargs
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
-type declaration_hook = Decl_kinds.locality -> GlobRef.t -> unit
+type hook_type = UState.t -> (Id.t * Constr.t) list -> Decl_kinds.locality -> GlobRef.t -> unit
+type declaration_hook = hook_type
+
let mk_hook hook = hook
-let call_hook ?hook ?fix_exn l c =
- try Option.iter (fun hook -> hook l c) hook
+
+let call_hook ?hook ?fix_exn uctx trans l c =
+ try Option.iter (fun hook -> hook uctx trans l c) hook
with e when CErrors.noncritical e ->
let e = CErrors.push e in
let e = Option.cata (fun fix -> fix e) e fix_exn in
@@ -174,7 +177,7 @@ let look_for_possibly_mutual_statements sigma = function
(* Saving a goal *)
-let save ?export_seff id const uctx do_guard (locality,poly,kind) hook =
+let save ?export_seff id const uctx do_guard (locality,poly,kind) hook universes =
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 +206,7 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook =
gr
in
definition_message id;
- call_hook ?hook locality r
+ call_hook ?hook universes [] locality r
with e when CErrors.noncritical e ->
let e = CErrors.push e in
iraise (fix_exn e)
@@ -230,10 +233,10 @@ let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_,
| Discharge ->
let impl = false in (* copy values from Vernacentries *)
let univs = match univs with
- | Polymorphic_const_entry (_, univs) ->
+ | Polymorphic_entry (_, univs) ->
(* What is going on here? *)
Univ.ContextSet.of_context univs
- | Monomorphic_const_entry univs -> univs
+ | Monomorphic_entry univs -> univs
in
let c = SectionLocalAssum ((t_i, univs),p,impl) in
let _ = declare_variable id (Lib.cwd(),c,k) in
@@ -289,7 +292,7 @@ let warn_let_as_axiom =
(fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++
spc () ++ strbrk "declared as an axiom.")
-let admit ?hook (id,k,e) pl () =
+let admit ?hook ctx (id,k,e) pl () =
let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in
let () = match k with
| Global, _, _ -> ()
@@ -297,16 +300,15 @@ let admit ?hook (id,k,e) pl () =
in
let () = assumption_message id in
Declare.declare_univ_binders (ConstRef kn) pl;
- call_hook ?hook Global (ConstRef kn)
+ call_hook ?hook ctx [] Global (ConstRef kn)
(* Starting a goal *)
-let universe_proof_terminator ?univ_hook compute_guard =
+let standard_proof_terminator ?(hook : declaration_hook option) compute_guard =
let open Proof_global in
make_terminator begin function
| Admitted (id,k,pe,ctx) ->
- let hook = Option.map (fun univ_hook -> univ_hook (Some ctx)) univ_hook in
- admit ?hook (id,k,pe) (UState.universe_binders ctx) ();
+ let () = admit ?hook ctx (id,k,pe) (UState.universe_binders ctx) () in
Feedback.feedback Feedback.AddedAxiom
| Proved (opaque,idopt, { id; entries=[const]; persistence; universes } ) ->
let is_opaque, export_seff = match opaque with
@@ -317,16 +319,12 @@ let universe_proof_terminator ?univ_hook compute_guard =
let id = match idopt with
| None -> id
| Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in
- let hook = Option.map (fun univ_hook -> univ_hook (Some universes)) univ_hook in
- save ~export_seff id const universes compute_guard persistence hook
+ let () = save ~export_seff id const universes compute_guard persistence hook universes in
+ ()
| Proved (opaque,idopt, _ ) ->
CErrors.anomaly Pp.(str "[universe_proof_terminator] close_proof returned more than one proof term")
end
-let standard_proof_terminator ?hook compute_guard =
- let univ_hook = Option.map (fun hook _ -> hook) hook in
- universe_proof_terminator ?univ_hook compute_guard
-
let initialize_named_context_for_proof () =
let sign = Global.named_context () in
List.fold_right
@@ -335,7 +333,7 @@ let initialize_named_context_for_proof () =
let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in
Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
-let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c =
+let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?(hook : declaration_hook option) c =
let terminator = match terminator with
| None -> standard_proof_terminator ?hook compute_guard
| Some terminator -> terminator ?hook compute_guard
@@ -348,20 +346,6 @@ let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c
let goals = [ Global.env_of_context sign , c ] in
Proof_global.start_proof sigma id ?pl kind goals terminator
-let start_proof_univs id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?univ_hook c =
- let terminator = match terminator with
- | None ->
- universe_proof_terminator ?univ_hook compute_guard
- | Some terminator -> terminator ?univ_hook compute_guard
- in
- let sign =
- match sign with
- | Some sign -> sign
- | None -> initialize_named_context_for_proof ()
- in
- let goals = [ Global.env_of_context sign , c ] in
- Proof_global.start_proof sigma id ?pl kind goals terminator
-
let rec_tac_initializer finite guard thms snl =
if finite then
match List.map (fun (id,(t,_)) -> (id,t)) thms with
@@ -394,11 +378,7 @@ let start_proof_with_initialization ?hook kind sigma decl recguard thms snl =
match thms with
| [] -> anomaly (Pp.str "No proof to start.")
| (id,(t,(_,imps)))::other_thms ->
- let hook ctx strength ref =
- let ctx = match ctx with
- | None -> UState.empty
- | Some ctx -> ctx
- in
+ let hook ctx _ strength ref =
let other_thms_data =
if List.is_empty other_thms then [] else
(* there are several theorems defined mutually *)
@@ -410,8 +390,8 @@ let start_proof_with_initialization ?hook kind sigma decl recguard thms snl =
let thms_data = (strength,ref,imps)::other_thms_data in
List.iter (fun (strength,ref,imps) ->
maybe_declare_manual_implicits false ref imps;
- call_hook ?hook strength ref) thms_data in
- start_proof_univs id ~pl:decl kind sigma t ~univ_hook:(fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard;
+ call_hook ?hook ctx [] strength ref) thms_data in
+ start_proof id ~pl:decl kind sigma t ~hook ~compute_guard:guard;
ignore (Proof_global.with_current_proof (fun _ p ->
match init_tac with
| None -> p,(true,[])
@@ -476,12 +456,19 @@ 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 = UState.const_univ_entry ~poly:(pi2 k) universes in
+ let ctx = UState.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, (typ, ctx), None), universes)
| None ->
let pftree = Proof_global.give_me_the_proof () in
- let id, k, typ = Pfedit.current_proof_statement () in
+ let gk = Proof_global.get_current_persistence () in
+ let Proof.{ name; poly; entry } = Proof.data pftree in
+ let typ = match Proofview.initial_goals entry with
+ | [typ] -> snd typ
+ | _ ->
+ CErrors.anomaly
+ ~label:"Lemmas.save_proof" (Pp.str "more than one statement.")
+ in
let typ = EConstr.Unsafe.to_constr typ in
let universes = Proof.((data pftree).initial_euctx) in
(* This will warn if the proof is complete *)
@@ -491,16 +478,15 @@ let save_proof ?proof = function
if not !keep_admitted_vars then None
else match Proof_global.get_used_variables(), pproofs with
| Some _ as x, _ -> x
- | None, (pproof, _) :: _ ->
+ | None, (pproof, _) :: _ ->
let env = Global.env () in
let ids_typ = Environ.global_vars_set env typ in
let ids_def = Environ.global_vars_set env pproof in
Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def))
| _ -> None in
let decl = Proof_global.get_universe_decl () in
- let poly = pi2 k in
let ctx = UState.check_univ_decl ~poly universes decl in
- Admitted(id,k,(sec_vars, (typ, ctx), None), universes)
+ Admitted(name,gk,(sec_vars, (typ, ctx), None), universes)
in
Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
| Vernacexpr.Proved (opaque,idopt) ->
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index a9a10a6e38..72c666e903 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -13,10 +13,29 @@ open Decl_kinds
type declaration_hook
-val mk_hook : (Decl_kinds.locality -> GlobRef.t -> unit) -> declaration_hook
-val call_hook :
- ?hook:declaration_hook -> ?fix_exn:Future.fix_exn ->
- Decl_kinds.locality -> GlobRef.t -> unit
+(* Hooks allow users of the API to perform arbitrary actions at
+ * proof/definition saving time. For example, to register a constant
+ * as a Coercion, perform some cleanup, update the search database,
+ * etc...
+ *
+ * Here, we use an extended hook type suitable for obligations /
+ * equations.
+ *)
+(** [hook_type] passes to the client:
+ - [ustate]: universe constraints obtained when the term was closed
+ - [(n1,t1),...(nm,tm)]: association list between obligation
+ name and the corresponding defined term (might be a constant,
+ but also an arbitrary term in the Expand case of obligations)
+ - [locality]: Locality of the original declaration
+ - [ref]: identifier of the origianl declaration
+ *)
+type hook_type = UState.t -> (Id.t * Constr.t) list -> Decl_kinds.locality -> GlobRef.t -> unit
+
+val mk_hook : hook_type -> declaration_hook
+val call_hook
+ : ?hook:declaration_hook
+ -> ?fix_exn:Future.fix_exn
+ -> hook_type
val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) ->
@@ -24,12 +43,6 @@ val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map
?compute_guard:Proof_global.lemma_possible_guards ->
?hook:declaration_hook -> EConstr.types -> unit
-val start_proof_univs : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
- ?terminator:(?univ_hook:(UState.t option -> declaration_hook) -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) ->
- ?sign:Environ.named_context_val ->
- ?compute_guard:Proof_global.lemma_possible_guards ->
- ?univ_hook:(UState.t option -> declaration_hook) -> EConstr.types -> unit
-
val start_proof_com :
program_mode:bool -> ?inference_hook:Pretyping.inference_hook ->
?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list ->
@@ -43,11 +56,6 @@ val start_proof_with_initialization :
(EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list ->
int list option -> unit
-val universe_proof_terminator :
- ?univ_hook:(UState.t option -> declaration_hook) ->
- Proof_global.lemma_possible_guards ->
- Proof_global.proof_terminator
-
val standard_proof_terminator :
?hook:declaration_hook -> Proof_global.lemma_possible_guards ->
Proof_global.proof_terminator
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index b20758dac5..38cdfc2d7a 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -20,15 +20,6 @@ open Pp
open CErrors
open Util
-type univ_declaration_hook = UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit
-let mk_univ_hook f = f
-let call_univ_hook ?univ_hook ?fix_exn uctx trans l c =
- try Option.iter (fun hook -> hook uctx trans l c) univ_hook
- with e when CErrors.noncritical e ->
- let e = CErrors.push e in
- let e = Option.cata (fun fix -> fix e) e fix_exn in
- iraise e
-
module NamedDecl = Context.Named.Declaration
let get_fix_exn, stm_get_fix_exn = Hook.make ()
@@ -321,7 +312,7 @@ type program_info_aux = {
prg_notations : notations ;
prg_kind : definition_kind;
prg_reduce : constr -> constr;
- prg_hook : univ_declaration_hook option;
+ prg_hook : Lemmas.declaration_hook option;
prg_opaque : bool;
prg_sign: named_context_val;
}
@@ -482,9 +473,9 @@ let declare_definition prg =
let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in
let () = progmap_remove prg in
let ubinders = UState.universe_binders uctx in
- let hook = Lemmas.mk_hook (fun l r -> call_univ_hook ?univ_hook:prg.prg_hook ~fix_exn uctx obls l r; ()) in
+ let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in
DeclareDef.declare_definition prg.prg_name
- prg.prg_kind ce ubinders prg.prg_implicits ~hook
+ prg.prg_kind ce ubinders prg.prg_implicits ?hook_data
let rec lam_index n t acc =
match Constr.kind t with
@@ -557,16 +548,18 @@ let declare_mutual_definition l =
mk_proof (mkCoFix (i,fixdecls))) 0 l
in
(* Declare the recursive definitions *)
- let univs = UState.const_univ_entry ~poly first.prg_ctx in
+ let univs = UState.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) UnivNames.empty_binders univs)
- fixnames fixdecls fixtypes fiximps in
- (* Declare notations *)
- List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
- Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
- let gr = List.hd kns in
- call_univ_hook ?univ_hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr;
- List.iter progmap_remove l; gr
+ let kns = List.map4
+ (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs)
+ fixnames fixdecls fixtypes fiximps
+ in
+ (* Declare notations *)
+ List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
+ Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
+ let gr = List.hd kns in
+ Lemmas.call_hook ?hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr;
+ List.iter progmap_remove l; gr
let decompose_lam_prod c ty =
let open Context.Rel.Declaration in
@@ -656,14 +649,14 @@ let declare_obligation prg obl body ty uctx =
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) ->
+ | Polymorphic_entry (_, uctx) ->
Some (DefinedObl (constant, Univ.UContext.instance uctx))
- | Monomorphic_const_entry _ ->
+ | Monomorphic_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) ?univ_hook sign n udecl b t ctx deps fixkind
+let init_prog_info ?(opaque = false) ?hook sign n udecl b t ctx deps fixkind
notations obls impls kind reduce =
let obls', b =
match b with
@@ -689,7 +682,7 @@ let init_prog_info ?(opaque = false) ?univ_hook sign n udecl b t ctx deps fixkin
prg_obligations = (obls', Array.length obls');
prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
prg_implicits = impls; prg_kind = kind; prg_reduce = reduce;
- prg_hook = univ_hook; prg_opaque = opaque;
+ prg_hook = hook; prg_opaque = opaque;
prg_sign = sign }
let map_cardinal m =
@@ -844,9 +837,9 @@ let solve_by_tac ?loc name evi t poly ctx =
warn_solve_errored ?loc err;
None
-let obligation_terminator ?univ_hook name num guard auto pf =
+let obligation_terminator ?hook name num guard auto pf =
let open Proof_global in
- let term = Lemmas.universe_proof_terminator ?univ_hook guard in
+ let term = Lemmas.standard_proof_terminator ?hook guard in
match pf with
| Admitted _ -> apply_terminator term pf
| Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin
@@ -879,7 +872,7 @@ let obligation_terminator ?univ_hook name num guard auto pf =
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 uctx = UState.univ_entry ~poly:(pi2 prg.prg_kind) ctx in
let (defined, obl) = declare_obligation prg obl body ty uctx in
let obls = Array.copy obls in
let () = obls.(num) <- obl in
@@ -912,7 +905,7 @@ let obligation_terminator ?univ_hook name num guard auto pf =
| Proved (_, _, _ ) ->
CErrors.anomaly Pp.(str "[obligation_terminator] close_proof returned more than one proof term")
-let obligation_hook prg obl num auto ctx' _ gr =
+let obligation_hook prg obl num auto ctx' _ _ gr =
let obls, rem = prg.prg_obligations in
let cst = match gr with GlobRef.ConstRef cst -> cst | _ -> assert false in
let transparent = evaluable_constant cst (Global.env ()) in
@@ -922,7 +915,6 @@ let obligation_hook prg obl num auto ctx' _ gr =
if not transparent then err_not_transp ()
| _ -> ()
in
- let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in
let inst, ctx' =
if not (pi2 prg.prg_kind) (* Not polymorphic *) then
(* The universe context was declared globally, we continue
@@ -969,11 +961,11 @@ let rec solve_obligation prg num tac =
let evd = Evd.from_ctx prg.prg_ctx in
let evd = Evd.update_sigma_env evd (Global.env ()) in
let auto n tac oblset = auto_solve_obligations n ~oblset tac in
- let terminator ?univ_hook guard =
+ let terminator ?hook guard =
Proof_global.make_terminator
- (obligation_terminator ?univ_hook prg.prg_name num guard auto) in
- let univ_hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
- let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~univ_hook in
+ (obligation_terminator ?hook prg.prg_name num guard auto) in
+ let hook = Lemmas.mk_hook (obligation_hook prg obl num auto) in
+ let () = Lemmas.start_proof ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in
let _ = Pfedit.by !default_tactic in
Option.iter (fun tac -> Proof_global.set_endline_tactic tac) tac
@@ -1010,7 +1002,7 @@ and solve_obligation_by_tac prg obls i tac =
(pi2 prg.prg_kind) (Evd.evar_universe_context evd) with
| None -> None
| Some (t, ty, ctx) ->
- let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in
+ let uctx = UState.univ_entry ~poly:(pi2 prg.prg_kind) ctx in
let prg = {prg with prg_ctx = ctx} in
let def, obl' = declare_obligation prg obl t ty uctx in
obls.(i) <- obl';
@@ -1110,10 +1102,10 @@ let show_term n =
let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
- ?(reduce=reduce) ?univ_hook ?(opaque = false) obls =
+ ?(reduce=reduce) ?hook ?(opaque = false) obls =
let sign = Lemmas.initialize_named_context_for_proof () in
let info = Id.print n ++ str " has type-checked" in
- let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce ?univ_hook in
+ let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce ?hook in
let obls,_ = prg.prg_obligations in
if Int.equal (Array.length obls) 0 then (
Flags.if_verbose Feedback.msg_info (info ++ str ".");
@@ -1130,13 +1122,13 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
?(kind=Global,false,Definition) ?(reduce=reduce)
- ?univ_hook ?(opaque = false) notations fixkind =
+ ?hook ?(opaque = false) notations fixkind =
let sign = Lemmas.initialize_named_context_for_proof () in
let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
List.iter
(fun (n, b, t, imps, obls) ->
let prg = init_prog_info sign ~opaque n univdecl (Some b) t ctx deps (Some fixkind)
- notations obls imps kind reduce ?univ_hook
+ notations obls imps kind reduce ?hook
in progmap_add n (CEphemeron.create prg)) l;
let _defined =
List.fold_left (fun finished x ->
@@ -1159,7 +1151,7 @@ let admit_prog prg =
match x.obl_body with
| None ->
let x = subst_deps_obl obls x in
- let ctx = Monomorphic_const_entry (UState.context_set prg.prg_ctx) in
+ let ctx = UState.univ_entry ~poly:false prg.prg_ctx in
let kn = Declare.declare_constant x.obl_name ~local:true
(ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural)
in
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 4eef668f56..c5720363b4 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -13,12 +13,6 @@ open Constr
open Evd
open Names
-type univ_declaration_hook
-val mk_univ_hook : (UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit) ->
- univ_declaration_hook
-val call_univ_hook : ?univ_hook:univ_declaration_hook -> ?fix_exn:Future.fix_exn ->
- UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit
-
(* This is a hack to make it possible for Obligations to craft a Qed
* behind the scenes. The fix_exn the Stm attaches to the Future proof
* is not available here, so we provide a side channel to get it *)
@@ -58,14 +52,19 @@ type progress = (* Resolution status of a program *)
val default_tactic : unit Proofview.tactic ref
-val add_definition : Names.Id.t -> ?term:constr -> types ->
- UState.t ->
- ?univdecl:UState.universe_decl -> (* Universe binders and constraints *)
- ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list ->
- ?kind:Decl_kinds.definition_kind ->
- ?tactic:unit Proofview.tactic ->
- ?reduce:(constr -> constr) ->
- ?univ_hook:univ_declaration_hook -> ?opaque:bool -> obligation_info -> progress
+val add_definition
+ : Names.Id.t
+ -> ?term:constr -> types
+ -> UState.t
+ -> ?univdecl:UState.universe_decl (* Universe binders and constraints *)
+ -> ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list
+ -> ?kind:Decl_kinds.definition_kind
+ -> ?tactic:unit Proofview.tactic
+ -> ?reduce:(constr -> constr)
+ -> ?hook:Lemmas.declaration_hook
+ -> ?opaque:bool
+ -> obligation_info
+ -> progress
type notations =
(lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
@@ -82,7 +81,7 @@ val add_mutual_definitions :
?tactic:unit Proofview.tactic ->
?kind:Decl_kinds.definition_kind ->
?reduce:(constr -> constr) ->
- ?univ_hook:univ_declaration_hook -> ?opaque:bool ->
+ ?hook:Lemmas.declaration_hook -> ?opaque:bool ->
notations ->
fixpoint_kind -> unit
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index 0e46df2320..994fad85f0 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -52,7 +52,7 @@ module Vernac_ =
let () =
let open Extend in
- let act_vernac v loc = Some (loc, v) in
+ let act_vernac v loc = Some CAst.(make ~loc v) in
let act_eoi _ loc = None in
let rule = [
Rule (Next (Stop, Atoken Tok.EOI), act_eoi);
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index fa251281dc..4bf7c9f7bd 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -26,7 +26,7 @@ module Vernac_ :
val rec_definition : (fixpoint_expr * decl_notation list) Entry.t
val noedit_mode : vernac_expr Entry.t
val command_entry : vernac_expr Entry.t
- val main_entry : (Loc.t * vernac_control) option Entry.t
+ val main_entry : vernac_control CAst.t option Entry.t
val red_expr : raw_red_expr Entry.t
val hint_info : Hints.hint_info_expr Entry.t
end
@@ -40,7 +40,7 @@ module Unsafe : sig
end
(** The main entry: reads an optional vernac command *)
-val main_entry : proof_mode option -> (Loc.t * vernac_control) option Entry.t
+val main_entry : proof_mode option -> vernac_control CAst.t option Entry.t
(** Grammar entry for tactics: proof mode(s).
By default Coq's grammar has an empty entry (non-terminal) for
diff --git a/vernac/record.ml b/vernac/record.ml
index 6b9a564b9e..0bd15e203b 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -277,8 +277,8 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f
let (mib,mip) = Global.lookup_inductive indsp in
let poly = Declareops.inductive_is_polymorphic mib in
let u = match ctx with
- | Polymorphic_const_entry (_, ctx) -> Univ.UContext.instance ctx
- | Monomorphic_const_entry ctx -> Univ.Instance.empty
+ | Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx
+ | Monomorphic_entry ctx -> Univ.Instance.empty
in
let paramdecls = Inductive.inductive_paramdecls (mib, u) in
let r = mkIndU (indsp,u) in
@@ -369,17 +369,16 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f
open Typeclasses
-let declare_structure finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data =
+let declare_structure ~cum finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data =
let nparams = List.length params in
let poly, ctx =
match univs with
- | Monomorphic_ind_entry ctx ->
- false, Monomorphic_const_entry Univ.ContextSet.empty
- | Polymorphic_ind_entry (nas, ctx) ->
- true, Polymorphic_const_entry (nas, ctx)
- | Cumulative_ind_entry (nas, cumi) ->
- true, Polymorphic_const_entry (nas, Univ.CumulativityInfo.univ_context cumi)
+ | Monomorphic_entry ctx ->
+ false, Monomorphic_entry Univ.ContextSet.empty
+ | Polymorphic_entry (nas, ctx) ->
+ true, Polymorphic_entry (nas, ctx)
in
+ let variance = if poly && cum then Some (InferCumulativity.dummy_variance ctx) else None in
let binder_name =
match name with
| None ->
@@ -427,6 +426,7 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
mind_entry_inds = blocks;
mind_entry_private = None;
mind_entry_universes = univs;
+ mind_entry_variance = variance;
}
in
let mie = InferCumulativity.infer_inductive (Global.env ()) mie in
@@ -472,8 +472,8 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
(DefinitionEntry class_entry, IsDefinition Definition)
in
let inst, univs = match univs with
- | Polymorphic_const_entry (_, uctx) -> Univ.UContext.instance uctx, univs
- | Monomorphic_const_entry _ -> Univ.Instance.empty, Monomorphic_const_entry Univ.ContextSet.empty
+ | Polymorphic_entry (_, uctx) -> Univ.UContext.instance uctx, univs
+ | Monomorphic_entry _ -> Univ.Instance.empty, Monomorphic_entry Univ.ContextSet.empty
in
let cstu = (cst, inst) in
let inst_type = appvectc (mkConstU cstu)
@@ -496,18 +496,8 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
in
[cref, [Name proj_name, sub, Some proj_cst]]
| _ ->
- let univs =
- match univs with
- | Polymorphic_const_entry (nas, univs) ->
- if cum then
- Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context univs)
- else
- Polymorphic_ind_entry (nas, univs)
- | Monomorphic_const_entry univs ->
- Monomorphic_ind_entry univs
- in
let record_data = [id, idbuild, arity, fieldimpls, fields, false, List.map (fun _ -> false) fields] in
- let inds = declare_structure Declarations.BiFinite ubinders univs paramimpls
+ let inds = declare_structure ~cum Declarations.BiFinite ubinders univs paramimpls
params template ~kind:Method ~name:[|binder_name|] record_data
in
let coers = List.map2 (fun coe pri ->
@@ -531,14 +521,14 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
in
let univs, ctx_context, fields =
match univs with
- | Polymorphic_const_entry (nas, univs) ->
+ | Polymorphic_entry (nas, univs) ->
let usubst, auctx = Univ.abstract_universes nas univs in
let usubst = Univ.make_instance_subst usubst 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
- | Monomorphic_const_entry _ ->
+ | Monomorphic_entry _ ->
Univ.AUContext.empty, ctx_context, fields
in
let map (impl, projs) =
@@ -670,21 +660,11 @@ let definition_structure udecl kind ~template cum poly finite records =
| _ ->
let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in
let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in
- let univs =
- match univs with
- | Polymorphic_const_entry (nas, univs) ->
- if cum then
- Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context univs)
- else
- Polymorphic_ind_entry (nas, univs)
- | Monomorphic_const_entry univs ->
- Monomorphic_ind_entry univs
- in
let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) =
let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in
let coe = List.map (fun coe -> not (Option.is_empty coe)) coers in
id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe
in
let data = List.map2 map data records in
- let inds = declare_structure finite ubinders univs implpars params template data in
+ let inds = declare_structure ~cum finite ubinders univs implpars params template data in
List.map (fun ind -> IndRef ind) inds
diff --git a/vernac/record.mli b/vernac/record.mli
index 04984030f7..9852840d12 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -16,7 +16,7 @@ val primitive_flag : bool ref
val declare_projections :
inductive ->
- Entries.constant_universes_entry ->
+ Entries.universes_entry ->
?kind:Decl_kinds.definition_object_kind ->
Id.t ->
bool list ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index eb263757e2..0d31992e98 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -16,7 +16,6 @@ open CAst
open Util
open Names
open Nameops
-open Term
open Tacmach
open Constrintern
open Prettyp
@@ -32,6 +31,7 @@ open Lemmas
open Locality
open Attributes
+module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
(** TODO: make this function independent of Ltac *)
@@ -133,22 +133,23 @@ let show_intro all =
*)
let make_cases_aux glob_ref =
+ let open Declarations in
match glob_ref with
| Globnames.IndRef ind ->
- let {Declarations.mind_nparams = np} , {Declarations.mind_nf_lc = tarr} = Global.lookup_inductive ind in
+ let mib, mip = Global.lookup_inductive ind in
Util.Array.fold_right_i
- (fun i typ l ->
- let al = List.rev (fst (decompose_prod typ)) in
- let al = Util.List.skipn np al in
+ (fun i (ctx, _) l ->
+ let al = Util.List.skipn (List.length mib.mind_params_ctxt) (List.rev ctx) in
let rec rename avoid = function
| [] -> []
- | (n,_)::l ->
+ | RelDecl.LocalDef _ :: l -> "_" :: rename avoid l
+ | RelDecl.LocalAssum (n, _)::l ->
let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n avoid in
Id.to_string n' :: rename (Id.Set.add n' avoid) l in
let al' = rename Id.Set.empty al in
let consref = ConstructRef (ith_constructor_of_inductive ind (i + 1)) in
(Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l)
- tarr []
+ mip.mind_nf_lc []
| _ -> raise Not_found
let make_cases s =
@@ -542,7 +543,7 @@ let vernac_definition_hook p = function
| Coercion ->
Some (Class.add_coercion_hook p)
| CanonicalStructure ->
- Some (Lemmas.mk_hook (fun _ -> Recordops.declare_canonical_structure))
+ Some (Lemmas.mk_hook (fun _ _ _ -> Recordops.declare_canonical_structure))
| SubClass ->
Some (Class.add_subclass_hook p)
| _ -> None
@@ -609,6 +610,11 @@ let vernac_assumption ~atts discharge kind l nl =
let status = ComAssumption.do_assumptions ~program_mode:atts.program kind nl l in
if not status then Feedback.feedback Feedback.AddedAxiom
+let is_polymorphic_inductive_cumulativity =
+ declare_bool_option_and_ref ~depr:false ~value:false
+ ~name:"Polymorphic inductive cumulativity"
+ ~key:["Polymorphic"; "Inductive"; "Cumulativity"]
+
let should_treat_as_cumulative cum poly =
match cum with
| Some VernacCumulative ->
@@ -617,7 +623,7 @@ let should_treat_as_cumulative cum poly =
| Some VernacNonCumulative ->
if poly then false
else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
- | None -> poly && Flags.is_polymorphic_inductive_cumulativity ()
+ | None -> poly && is_polymorphic_inductive_cumulativity ()
let get_uniform_inductive_parameters =
Goptions.declare_bool_option_and_ref
@@ -1564,14 +1570,6 @@ let () =
optwrite = (fun b -> Flags.raw_print := b) }
let () =
- declare_bool_option
- { optdepr = false;
- optname = "Polymorphic inductive cumulativity";
- optkey = ["Polymorphic"; "Inductive"; "Cumulativity"];
- optread = Flags.is_polymorphic_inductive_cumulativity;
- optwrite = Flags.make_polymorphic_inductive_cumulativity }
-
-let () =
declare_int_option
{ optdepr = false;
optname = "the level of inlining during functor application";
@@ -1785,7 +1783,7 @@ let vernac_check_may_eval ~atts redexp glopt rc =
else
let c = EConstr.to_constr sigma c in
(* OK to call kernel which does not support evars *)
- Termops.on_judgment EConstr.of_constr (Arguments_renaming.rename_typing env c)
+ Environ.on_judgment EConstr.of_constr (Arguments_renaming.rename_typing env c)
in
let pp = match redexp with
| None ->
@@ -2150,7 +2148,7 @@ let vernac_load interp fname =
else
None
in
- interp (snd (parse_sentence proof_mode input));
+ interp (parse_sentence proof_mode input).CAst.v;
done
with End_of_input -> ()
end;
@@ -2380,6 +2378,8 @@ let locate_if_not_already ?loc (e, info) =
exception HasNotFailed
exception HasFailed of Pp.t
+let test_mode = ref false
+
(* XXX STATE: this type hints that restoring the state should be the
caller's responsibility *)
let with_fail st b f =
@@ -2405,7 +2405,7 @@ let with_fail st b f =
| HasNotFailed ->
user_err ~hdr:"Fail" (str "The command has not failed!")
| HasFailed msg ->
- if not !Flags.quiet || !Flags.test_mode then Feedback.msg_info
+ if not !Flags.quiet || !test_mode then Feedback.msg_info
(str "The command has indeed failed with message:" ++ fnl () ++ msg)
| _ -> assert false
end
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 4fbd3849b0..f43cec48e9 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -41,3 +41,7 @@ val command_focus : unit Proof.focus_kind
val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr ->
Evd.evar_map * Redexpr.red_expr) Hook.t
+
+(* Flag set when the test-suite is called. Its only effect to display
+ verbose information for `Fail` *)
+val test_mode : bool ref
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 05:05:38 +0000