aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--library/decl_kinds.ml2
-rw-r--r--plugins/derive/derive.ml5
-rw-r--r--plugins/funind/functional_principles_proofs.ml4
-rw-r--r--plugins/funind/functional_principles_types.ml6
-rw-r--r--plugins/funind/indfun_common.ml2
-rw-r--r--plugins/funind/invfun.ml8
-rw-r--r--plugins/funind/recdef.ml8
-rw-r--r--plugins/ltac/rewrite.ml5
-rw-r--r--proofs/pfedit.ml8
-rw-r--r--proofs/pfedit.mli16
-rw-r--r--proofs/proof_global.ml14
-rw-r--r--proofs/proof_global.mli3
-rw-r--r--tactics/abstract.ml6
-rw-r--r--vernac/classes.ml4
-rw-r--r--vernac/comFixpoint.ml2
-rw-r--r--vernac/lemmas.ml55
-rw-r--r--vernac/lemmas.mli4
-rw-r--r--vernac/obligations.ml21
-rw-r--r--vernac/vernacentries.ml9
19 files changed, 103 insertions, 79 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 0e2ef95739..4b20016ab2 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -67,7 +67,7 @@ type goal_object_kind =
| DefinitionBody of definition_object_kind
| Proof of theorem_kind
-type goal_kind = locality * polymorphic * goal_object_kind
+type goal_kind = locality * goal_object_kind
(** Kinds used in library *)
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 22e20e2c52..8c2cf3c553 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -19,7 +19,8 @@ let start_deriving f suchthat name : Lemmas.t =
let env = Global.env () in
let sigma = Evd.from_env env in
- let kind = Decl_kinds.(Global ImportDefaultBehavior,false,DefinitionBody Definition) in
+ let poly = false in
+ let kind = Decl_kinds.(Global ImportDefaultBehavior,DefinitionBody Definition) in
(* create a sort variable for the type of [f] *)
(* spiwack: I don't know what the rigidity flag does, picked the one
@@ -40,7 +41,7 @@ let start_deriving f suchthat name : Lemmas.t =
in
let info = Lemmas.Info.make ~proof_ending:(Lemmas.Proof_ending.(End_derive {f; name})) () in
- let lemma = Lemmas.start_dependent_lemma ~name ~kind ~info goals in
+ let lemma = Lemmas.start_dependent_lemma ~name ~poly ~kind ~info goals in
Lemmas.pf_map (Proof_global.map_proof begin fun p ->
Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
end) lemma
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 9c593a55d8..c37e6f7402 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -995,8 +995,8 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
Ensures by: obvious
i*)
~name:(mk_equation_id f_id)
- ~kind:Decl_kinds.(Global ImportDefaultBehavior, false, Proof Theorem)
-
+ ~poly:false
+ ~kind:(Decl_kinds.(Global ImportDefaultBehavior, Proof Theorem))
evd
lemma_type
in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 1154198d43..1b447bd26a 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -308,8 +308,10 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
evd := sigma;
let hook = DeclareDef.Hook.make (hook new_principle_type) in
let lemma =
- Lemmas.start_lemma ~name:new_princ_name
- ~kind:Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
+ Lemmas.start_lemma
+ ~name:new_princ_name
+ ~poly:false
+ ~kind:(Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem))
!evd
(EConstr.of_constr new_principle_type)
in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 17c79e0e6c..a5a07934ac 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -123,7 +123,7 @@ open Declare
let definition_message = Declare.definition_message
-let save id const ?hook uctx (locality,_,kind) =
+let save id const ?hook uctx (locality,kind) =
let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in
let r = match locality with
| Discharge ->
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 48b5e56635..e5b0a5d032 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -805,7 +805,8 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
let (typ,_) = lemmas_types_infos.(i) in
let lemma = Lemmas.start_lemma
~name:lem_id
- ~kind:Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
+ ~poly:false
+ ~kind:Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem)
!evd
typ in
let lemma = fst @@ Lemmas.by
@@ -866,8 +867,9 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
i*)
let lem_id = mk_complete_id f_id in
let lemma = Lemmas.start_lemma ~name:lem_id
- ~kind:Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) sigma
- (fst lemmas_types_infos.(i)) in
+ ~poly:false
+ ~kind:Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem) sigma
+ (fst lemmas_types_infos.(i)) in
let lemma = fst (Lemmas.by
(Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
(proving_tac i))) lemma) in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index c97b39ff79..187d907dc5 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1370,7 +1370,8 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) () in
let lemma = Lemmas.start_lemma
~name:na
- ~kind:Decl_kinds.(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma) ~info
+ ~poly:false (* FIXME *)
+ ~kind:Decl_kinds.(Global ImportDefaultBehavior, Proof Lemma) ~info
sigma gls_type in
let lemma = if Indfun_common.is_strict_tcc ()
then
@@ -1411,7 +1412,8 @@ let com_terminate
let start_proof env ctx (tac_start:tactic) (tac_end:tactic) =
let info = Lemmas.Info.make ~hook () in
let lemma = Lemmas.start_lemma ~name:thm_name
- ~kind:(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma)
+ ~poly:false (*FIXME*)
+ ~kind:(Global ImportDefaultBehavior, Proof Lemma)
~sign:(Environ.named_context_val env)
~info
ctx
@@ -1460,7 +1462,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
let evd = Evd.from_ctx uctx in
let f_constr = constr_of_monomorphic_global f_ref in
let equation_lemma_type = subst1 f_constr equation_lemma_type in
- let lemma = Lemmas.start_lemma ~name:eq_name ~kind:(Global ImportDefaultBehavior, false, Proof Lemma) ~sign evd
+ let lemma = Lemmas.start_lemma ~name:eq_name ~poly:false ~kind:(Global ImportDefaultBehavior, Proof Lemma) ~sign evd
(EConstr.of_constr equation_lemma_type) in
let lemma = fst @@ Lemmas.by
(Proofview.V82.tactic (start_equation f_ref terminate_ref
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 49265802ae..d87b7a1770 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1994,7 +1994,8 @@ let add_morphism_interactive atts m n : Lemmas.t =
let env = Global.env () in
let evd = Evd.from_env env in
let uctx, instance = build_morphism_signature env evd m in
- let kind = Decl_kinds.Global Decl_kinds.ImportDefaultBehavior, atts.polymorphic,
+ let poly = atts.polymorphic in
+ let kind = Decl_kinds.(Global ImportDefaultBehavior),
Decl_kinds.DefinitionBody Decl_kinds.Instance
in
let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
@@ -2010,7 +2011,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
let info = Lemmas.Info.make ~hook () in
Flags.silently
(fun () ->
- let lemma = Lemmas.start_lemma ~name:instance_id ~kind ~info (Evd.from_ctx uctx) (EConstr.of_constr instance) in
+ let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~kind ~info (Evd.from_ctx uctx) (EConstr.of_constr instance) in
fst (Lemmas.by (Tacinterp.interp tac) lemma)) ()
let add_morphism atts binders m s n =
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index d00f2c4803..64d21be7e8 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -116,10 +116,10 @@ open Decl_kinds
let next = let n = ref 0 in fun () -> incr n; !n
-let build_constant_by_tactic id ctx sign ?(goal_kind = Global ImportDefaultBehavior, false, Proof Theorem) typ tac =
+let build_constant_by_tactic id ctx sign ~poly ?(goal_kind = Global ImportDefaultBehavior, Proof Theorem) typ tac =
let evd = Evd.from_ctx ctx in
let goals = [ (Global.env_of_context sign , typ) ] in
- let pf = Proof_global.start_proof evd id UState.default_univ_decl goal_kind goals in
+ let pf = Proof_global.start_proof evd id ~poly UState.default_univ_decl goal_kind goals in
try
let pf, status = by tac pf in
let open Proof_global in
@@ -137,9 +137,9 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global ImportDefaultBehav
let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
let sign = val_of_named_context (named_context env) in
- let gk = Global ImportDefaultBehavior, poly, Proof Theorem in
+ let gk = Global ImportDefaultBehavior, Proof Theorem in
let ce, status, univs =
- build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac in
+ build_constant_by_tactic id sigma sign ~poly ~goal_kind:gk typ tac in
let body, eff = Future.force ce.Proof_global.proof_entry_body in
let (cb, ctx) =
if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index d01704926a..51cb3ca0ee 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -58,14 +58,18 @@ val use_unification_heuristics : unit -> bool
[tac]. The return boolean, if [false] indicates the use of an unsafe
tactic. *)
-val build_constant_by_tactic :
- Id.t -> UState.t -> named_context_val -> ?goal_kind:goal_kind ->
- EConstr.types -> unit Proofview.tactic ->
- Evd.side_effects Proof_global.proof_entry * bool *
- UState.t
+val build_constant_by_tactic
+ : Id.t
+ -> UState.t
+ -> named_context_val
+ -> poly:bool
+ -> ?goal_kind:goal_kind
+ -> EConstr.types
+ -> unit Proofview.tactic
+ -> Evd.side_effects Proof_global.proof_entry * bool * UState.t
val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic ->
- EConstr.types -> unit Proofview.tactic ->
+ EConstr.types -> unit Proofview.tactic ->
constr * bool * UState.t
val refine_by_tactic
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 2f7e5d618a..22f818edbb 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -39,6 +39,7 @@ type 'a proof_entry = {
type proof_object =
{ id : Names.Id.t
; entries : Evd.side_effects proof_entry list
+ ; poly : bool
; persistence : Decl_kinds.goal_kind
; universes: UState.t
; udecl : UState.universe_decl
@@ -69,7 +70,8 @@ let map_fold_proof_endline f ps =
| None -> Proofview.tclUNIT ()
| Some tac ->
let open Geninterp in
- let ist = { lfun = Id.Map.empty; poly = pi2 ps.strength; extra = TacStore.empty } in
+ let {Proof.poly} = Proof.data ps.proof in
+ let ist = { lfun = Id.Map.empty; poly; extra = TacStore.empty } in
let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in
let tac = Geninterp.interp tag ist tac in
Ftactic.run tac (fun _ -> Proofview.tclUNIT ())
@@ -92,16 +94,16 @@ let set_endline_tactic tac ps =
end of the proof to close the proof. The proof is started in the
evar map [sigma] (which can typically contain universe
constraints), and with universe bindings pl. *)
-let start_proof sigma name udecl kind goals =
- { proof = Proof.start ~name ~poly:(pi2 kind) sigma goals
+let start_proof sigma name udecl ~poly kind goals =
+ { proof = Proof.start ~name ~poly sigma goals
; endline_tactic = None
; section_vars = None
; udecl
; strength = kind
}
-let start_dependent_proof name udecl kind goals =
- { proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals
+let start_dependent_proof name udecl ~poly kind goals =
+ { proof = Proof.dependent_start ~name ~poly goals
; endline_tactic = None
; section_vars = None
; udecl
@@ -254,7 +256,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
proof_entry_universes = univs; }
in
let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in
- { id = name; entries = entries; persistence = strength; universes; udecl }
+ { id = name; entries = entries; poly; persistence = strength; universes; udecl }
let return_proof ?(allow_partial=false) ps =
let { proof } = ps in
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 3baa58084d..5bfed948ba 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -46,6 +46,7 @@ type 'a proof_entry = {
type proof_object =
{ id : Names.Id.t
; entries : Evd.side_effects proof_entry list
+ ; poly : bool
; persistence : Decl_kinds.goal_kind
; universes: UState.t
; udecl : UState.universe_decl
@@ -65,6 +66,7 @@ val start_proof
: Evd.evar_map
-> Names.Id.t
-> UState.universe_decl
+ -> poly:bool
-> Decl_kinds.goal_kind
-> (Environ.env * EConstr.types) list
-> t
@@ -74,6 +76,7 @@ val start_proof
val start_dependent_proof
: Names.Id.t
-> UState.universe_decl
+ -> poly:bool
-> Decl_kinds.goal_kind
-> Proofview.telescope
-> t
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index e4fa5e84b4..68a2a0afe0 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -103,8 +103,8 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
question, how does abstract behave when discharge is local for example?
*)
let goal_kind, suffix = if opaque
- then (Global ImportDefaultBehavior,poly,Proof Theorem), "_subproof"
- else (Global ImportDefaultBehavior,poly,DefinitionBody Definition), "_subterm" in
+ then (Global ImportDefaultBehavior,Proof Theorem), "_subproof"
+ else (Global ImportDefaultBehavior,DefinitionBody Definition), "_subterm" in
let id, goal_kind = name_op_to_name ~name_op ~name ~goal_kind suffix in
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
@@ -141,7 +141,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in
let ectx = Evd.evar_universe_context evd in
let (const, safe, ectx) =
- try Pfedit.build_constant_by_tactic ~goal_kind id ectx secsign concl solve_tac
+ try Pfedit.build_constant_by_tactic ~poly ~goal_kind id ectx secsign concl solve_tac
with Logic_monad.TacticFailure e as src ->
(* if the tactic [tac] fails, it reports a [TacticFailure e],
which is an error irrelevant to the proof system (in fact it
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 37af8e1f55..bb5ebd7148 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -373,10 +373,10 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t
the refinement manually.*)
let gls = List.rev (Evd.future_goals sigma) in
let sigma = Evd.reset_future_goals sigma in
- let kind = Decl_kinds.(Global ImportDefaultBehavior, poly, DefinitionBody Instance) in
+ let kind = Decl_kinds.Global ImportDefaultBehavior, Decl_kinds.DefinitionBody Decl_kinds.Instance in
let hook = DeclareDef.Hook.make (fun _ _ _ -> instance_hook pri global imps ?hook) in
let info = Lemmas.Info.make ~hook () in
- let lemma = Lemmas.start_lemma ~name:id ~kind ~udecl ~info sigma (EConstr.of_constr termtype) in
+ let lemma = Lemmas.start_lemma ~name:id ~poly ~kind ~udecl ~info sigma (EConstr.of_constr termtype) in
(* spiwack: I don't know what to do with the status here. *)
let lemma =
if not (Option.is_empty term) then
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 31c2053148..6d9aa746b9 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -269,7 +269,7 @@ let declare_fixpoint_interactive_generic ?indexes local poly ((fixnames,_fixrs,f
Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in
let evd = Evd.from_ctx ctx in
let lemma =
- Lemmas.start_lemma_with_initialization ~kind:(local,poly,DefinitionBody fix_kind) ~udecl
+ Lemmas.start_lemma_with_initialization ~poly ~kind:(local,DefinitionBody fix_kind) ~udecl
evd (Some(cofix,indexes,init_tac)) thms None in
(* Declare notations *)
List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index c3dfdd1c0f..d323493c11 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -246,7 +246,7 @@ let check_name_freshness locality {CAst.loc;v=id} : unit =
then
user_err ?loc (Id.print id ++ str " already exists.")
-let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i
+let save_remaining_recthms env sigma ~poly (locality,kind) norm univs body opaq i
{ Recthm.name; typ; impargs } =
let t_i = norm typ in
let k = IsAssumption Conjectural in
@@ -261,7 +261,7 @@ let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i
Univ.ContextSet.of_context univs
| Monomorphic_entry univs -> univs
in
- let c = SectionLocalAssum ((t_i, univs),p,impl) in
+ let c = SectionLocalAssum ((t_i, univs),poly,impl) in
let _ = declare_variable name (Lib.cwd(),c,k) in
(VarRef name,impargs)
| Global local ->
@@ -338,19 +338,19 @@ module Stack = struct
end
(* Starting a goal *)
-let start_lemma ~name ~kind
+let start_lemma ~name ~poly ~kind
?(udecl=UState.default_univ_decl)
?(sign=initialize_named_context_for_proof())
?(info=Info.make ())
sigma c =
let goals = [ Global.env_of_context sign , c ] in
- let proof = Proof_global.start_proof sigma name udecl kind goals in
+ let proof = Proof_global.start_proof sigma name udecl ~poly kind goals in
{ proof ; info }
-let start_dependent_lemma ~name ~kind
+let start_dependent_lemma ~name ~poly ~kind
?(udecl=UState.default_univ_decl)
?(info=Info.make ()) telescope =
- let proof = Proof_global.start_dependent_proof name udecl kind telescope in
+ let proof = Proof_global.start_dependent_proof name udecl ~poly kind telescope in
{ proof; info }
let rec_tac_initializer finite guard thms snl =
@@ -367,7 +367,7 @@ let rec_tac_initializer finite guard thms snl =
| (id,n,_)::l -> Tactics.mutual_fix id n l 0
| _ -> assert false
-let start_lemma_with_initialization ?hook ~kind ~udecl sigma recguard thms snl =
+let start_lemma_with_initialization ?hook ~poly ~kind ~udecl sigma recguard thms snl =
let intro_tac { Recthm.args; _ } = Tactics.auto_intros_tac args in
let init_tac, compute_guard = match recguard with
| Some (finite,guard,init_tac) ->
@@ -392,13 +392,13 @@ let start_lemma_with_initialization ?hook ~kind ~udecl sigma recguard thms snl =
; other_thms
; proof_ending = CEphemeron.create Proof_ending.Regular
} in
- let lemma = start_lemma ~name ~kind ~udecl ~info sigma typ in
+ let lemma = start_lemma ~name ~poly ~kind ~udecl ~info sigma typ in
pf_map (Proof_global.map_proof (fun p ->
match init_tac with
| None -> p
| Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p)) lemma
-let start_lemma_com ~program_mode ~kind ?inference_hook ?hook thms =
+let start_lemma_com ~program_mode ~poly ~kind ?inference_hook ?hook thms =
let env0 = Global.env () in
let decl = fst (List.hd thms) in
let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in
@@ -409,7 +409,7 @@ let start_lemma_com ~program_mode ~kind ?inference_hook ?hook thms =
let hook = inference_hook in
let evd = solve_remaining_evars ?hook flags env evd in
let ids = List.map RelDecl.get_name ctx in
- check_name_freshness (pi1 kind) id;
+ check_name_freshness (fst kind) id;
(* XXX: The nf_evar is critical !! *)
evd, (id.CAst.v,
(Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx),
@@ -424,14 +424,14 @@ let start_lemma_com ~program_mode ~kind ?inference_hook ?hook thms =
let () =
let open UState in
if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then
- ignore (Evd.check_univ_decl ~poly:(pi2 kind) evd udecl)
+ ignore (Evd.check_univ_decl ~poly evd udecl)
in
let evd =
- if pi2 kind then evd
+ if poly then evd
else (* We fix the variables to ensure they won't be lowered to Set *)
Evd.fix_undefined_variables evd
in
- start_lemma_with_initialization ?hook ~kind evd ~udecl recguard thms snl
+ start_lemma_with_initialization ?hook ~poly ~kind evd ~udecl recguard thms snl
(************************************************************************)
(* Admitting a lemma-like constant *)
@@ -449,19 +449,19 @@ let warn_let_as_axiom =
(* This declares implicits and calls the hooks for all the theorems,
including the main one *)
-let process_recthms ?fix_exn ?hook env sigma ctx decl strength ref imps other_thms =
+let process_recthms ?fix_exn ?hook env sigma ctx decl ~poly strength ref imps other_thms =
let other_thms_data =
if List.is_empty other_thms then [] else
(* there are several theorems defined mutually *)
let body,opaq = retrieve_first_recthm ctx ref in
let norm c = EConstr.to_constr (Evd.from_ctx ctx) c in
let body = Option.map EConstr.of_constr body in
- let uctx = UState.check_univ_decl ~poly:(pi2 strength) ctx decl in
- List.map_i (save_remaining_recthms env sigma strength norm uctx body opaq) 1 other_thms in
+ let uctx = UState.check_univ_decl ~poly ctx decl in
+ List.map_i (save_remaining_recthms env sigma ~poly strength norm uctx body opaq) 1 other_thms in
let thms_data = (ref,imps)::other_thms_data in
List.iter (fun (ref,imps) ->
maybe_declare_manual_implicits false ref imps;
- DeclareDef.Hook.call ?fix_exn ?hook ctx [] (pi1 strength) ref) thms_data
+ DeclareDef.Hook.call ?fix_exn ?hook ctx [] (fst strength) ref) thms_data
let get_keep_admitted_vars =
Goptions.declare_bool_option_and_ref
@@ -470,7 +470,7 @@ let get_keep_admitted_vars =
~key:["Keep"; "Admitted"; "Variables"]
~value:true
-let finish_admitted env sigma id (scope,poly,kind) pe ctx hook udecl impargs other_thms =
+let finish_admitted env sigma id ~poly (scope,kind) pe ctx hook udecl impargs other_thms =
let local = match scope with
| Global local -> local
| Discharge -> warn_let_as_axiom id; ImportNeedQualified
@@ -479,7 +479,7 @@ let finish_admitted env sigma id (scope,poly,kind) pe ctx hook udecl impargs oth
let () = assumption_message id in
Declare.declare_univ_binders (ConstRef kn) (UState.universe_binders ctx);
(* This takes care of the implicits and hook for the current constant*)
- process_recthms ?fix_exn:None ?hook env sigma ctx udecl (Global local,poly,kind) (ConstRef kn) impargs other_thms;
+ process_recthms ?fix_exn:None ?hook env sigma ctx udecl ~poly (Global local,kind) (ConstRef kn) impargs other_thms;
Feedback.feedback Feedback.AddedAxiom
let save_lemma_admitted ?proof ~(lemma : t) =
@@ -489,14 +489,17 @@ let save_lemma_admitted ?proof ~(lemma : t) =
| Some ({ id; entries; persistence = k; universes; udecl }, { Info.hook; impargs; other_thms; _} ) ->
if List.length entries <> 1 then
user_err Pp.(str "Admitted does not support multiple statements");
- let { proof_entry_secctx; proof_entry_type } = List.hd entries in
+ let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
if proof_entry_type = None then
user_err Pp.(str "Admitted requires an explicit statement");
+ let poly = match proof_entry_universes with
+ | Entries.Monomorphic_entry _ -> false
+ | Entries.Polymorphic_entry (_, _) -> true in
let typ = Option.get proof_entry_type in
- let ctx = UState.univ_entry ~poly:(pi2 k) universes in
+ let ctx = UState.univ_entry ~poly universes in
let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in
let sigma = Evd.from_env env in
- finish_admitted env sigma id k (sec_vars, (typ, ctx), None) universes hook udecl impargs other_thms
+ finish_admitted env sigma id k (sec_vars, (typ, ctx), None) universes hook ~poly udecl impargs other_thms
| None ->
let pftree = Proof_global.get_proof lemma.proof in
let gk = Proof_global.get_persistence lemma.proof in
@@ -526,7 +529,7 @@ let save_lemma_admitted ?proof ~(lemma : t) =
let { Info.hook; impargs; other_thms } = lemma.info in
let { Proof.sigma } = Proof.data (Proof_global.get_proof lemma.proof) in
let ctx = UState.check_univ_decl ~poly universes udecl in
- finish_admitted env sigma name gk (sec_vars, (typ, ctx), None) universes hook udecl impargs other_thms
+ finish_admitted env sigma name gk (sec_vars, (typ, ctx), None) universes hook ~poly udecl impargs other_thms
(************************************************************************)
(* Saving a lemma-like constant *)
@@ -536,7 +539,7 @@ let finish_proved env sigma opaque idopt po info =
let open Proof_global in
let { Info.hook; compute_guard; impargs; other_thms } = info in
match po with
- | { id; entries=[const]; persistence=locality,poly,kind; universes; udecl } ->
+ | { id; entries=[const]; persistence=locality,kind; universes; udecl; poly } ->
let is_opaque = match opaque with
| Transparent -> false
| Opaque -> true
@@ -570,7 +573,7 @@ let finish_proved env sigma opaque idopt po info =
in
definition_message id;
(* This takes care of the implicits and hook for the current constant*)
- process_recthms ~fix_exn ?hook env sigma universes udecl (locality,poly,kind) r impargs other_thms
+ process_recthms ~fix_exn ?hook env sigma universes udecl ~poly (locality,kind) r impargs other_thms
with e when CErrors.noncritical e ->
let e = CErrors.push e in
iraise (fix_exn e)
@@ -627,7 +630,7 @@ let finish_proved_equations opaque lid proof_obj hook i types wits sigma0 =
let open Decl_kinds in
let obls = ref 1 in
- let kind = match pi3 proof_obj.Proof_global.persistence with
+ let kind = match snd proof_obj.Proof_global.persistence with
| DefinitionBody d -> IsDefinition d
| Proof p -> IsProof p
in
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 28b9c38072..1a8b1f2f30 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -93,6 +93,7 @@ end
(** Starts the proof of a constant *)
val start_lemma
: name:Id.t
+ -> poly:bool
-> kind:goal_kind
-> ?udecl:UState.universe_decl
-> ?sign:Environ.named_context_val
@@ -103,6 +104,7 @@ val start_lemma
val start_dependent_lemma
: name:Id.t
+ -> poly:bool
-> kind:goal_kind
-> ?udecl:UState.universe_decl
-> ?info:Info.t
@@ -114,6 +116,7 @@ type lemma_possible_guards = int list list
(** Pretty much internal, only used in ComFixpoint *)
val start_lemma_with_initialization
: ?hook:DeclareDef.Hook.t
+ -> poly:bool
-> kind:goal_kind
-> udecl:UState.universe_decl
-> Evd.evar_map
@@ -127,6 +130,7 @@ val default_thm_id : Names.Id.t
(** Main [Lemma foo args : type.] command *)
val start_lemma_com
: program_mode:bool
+ -> poly:bool
-> kind:goal_kind
-> ?inference_hook:Pretyping.inference_hook
-> ?hook:DeclareDef.Hook.t
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 4e4f80fd71..b2c5520c0b 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -388,16 +388,14 @@ let deps_remaining obls deps =
deps []
-let goal_kind poly =
- Decl_kinds.(Global ImportNeedQualified, poly, DefinitionBody Definition)
+let goal_kind = Decl_kinds.(Global ImportNeedQualified, DefinitionBody Definition)
+let goal_proof_kind = Decl_kinds.(Global ImportNeedQualified, Proof Lemma)
-let goal_proof_kind poly =
- Decl_kinds.(Global ImportNeedQualified, poly, Proof Lemma)
-
-let kind_of_obligation poly o =
+let kind_of_obligation o =
match o with
- | Evar_kinds.Define false | Evar_kinds.Expand -> goal_kind poly
- | _ -> goal_proof_kind poly
+ | Evar_kinds.Define false
+ | Evar_kinds.Expand -> goal_kind
+ | _ -> goal_proof_kind
let rec string_of_list sep f = function
[] -> ""
@@ -415,7 +413,7 @@ let solve_by_tac ?loc name evi t poly ctx =
try
let (entry,_,ctx') =
Pfedit.build_constant_by_tactic
- id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl t in
+ id ~poly ~goal_kind ctx evi.evar_hyps evi.evar_concl t in
let env = Global.env () in
let (body, eff) = Future.force entry.Proof_global.proof_entry_body in
let body = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in
@@ -486,14 +484,15 @@ let rec solve_obligation prg num tac =
++ str (string_of_list ", " (fun x -> string_of_int (succ x)) remaining));
in
let obl = subst_deps_obl obls obl in
- let kind = kind_of_obligation (pi2 prg.prg_kind) (snd obl.obl_status) in
+ let kind = kind_of_obligation (snd obl.obl_status) in
let evd = Evd.from_ctx prg.prg_ctx in
let evd = Evd.update_sigma_env evd (Global.env ()) in
let auto n oblset tac = auto_solve_obligations n ~oblset tac in
let proof_ending = Lemmas.Proof_ending.End_obligation (DeclareObl.{name = prg.prg_name; num; auto}) in
let hook = DeclareDef.Hook.make (obligation_hook prg obl num auto) in
let info = Lemmas.Info.make ~hook ~proof_ending () in
- let lemma = Lemmas.start_lemma ~sign:prg.prg_sign ~name:obl.obl_name ~kind ~info evd (EConstr.of_constr obl.obl_type) in
+ let poly = pi2 prg.prg_kind in
+ let lemma = Lemmas.start_lemma ~sign:prg.prg_sign ~name:obl.obl_name ~poly ~kind ~info evd (EConstr.of_constr obl.obl_type) in
let lemma = fst @@ Lemmas.by !default_tactic lemma in
let lemma = Option.cata (fun tac -> Lemmas.set_endline_tactic tac lemma) lemma tac in
lemma
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index da8808ccaa..d1377fecc5 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -560,7 +560,7 @@ let () =
(***********)
(* Gallina *)
-let start_proof_and_print ~program_mode ?hook k l =
+let start_proof_and_print ~program_mode ~poly ?hook k l =
let inference_hook =
if program_mode then
let hook env sigma ev =
@@ -582,7 +582,7 @@ let start_proof_and_print ~program_mode ?hook k l =
in Some hook
else None
in
- start_lemma_com ~program_mode ?inference_hook ?hook ~kind:k l
+ start_lemma_com ~program_mode ?inference_hook ?hook ~poly ~kind:k l
let vernac_definition_hook p = function
| Coercion ->
@@ -614,8 +614,9 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
let local = enforce_locality_exp atts.locality discharge in
let hook = vernac_definition_hook atts.polymorphic kind in
let program_mode = atts.program in
+ let poly = atts.polymorphic in
let name = vernac_definition_name lid local in
- start_proof_and_print ~program_mode (local, atts.polymorphic, DefinitionBody kind) ?hook [(name, pl), (bl, t)]
+ start_proof_and_print ~program_mode ~poly (local, DefinitionBody kind) ?hook [(name, pl), (bl, t)]
let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt =
let open DefAttributes in
@@ -638,7 +639,7 @@ let vernac_start_proof ~atts kind l =
let local = enforce_locality_exp atts.locality NoDischarge in
if Dumpglob.dump () then
List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
- start_proof_and_print ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l
+ start_proof_and_print ~program_mode:atts.program ~poly:atts.polymorphic (local, Proof kind) l
let vernac_end_proof ?stack ?proof = let open Vernacexpr in function
| Admitted ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:36:11 +0000