From a8b3c907cb2d6da16bdeea10b943552dc9efc0ed Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 5 Jun 2019 17:48:46 +0200 Subject: [proof] Move proofs that have an associated constant to `Lemmas` The main idea of this PR is to distinguish the types of "proof object" `Proof_global.t` and the type of "proof object associated to a constant, the new `Lemmas.t`. This way, we can move the terminator setup to the higher layer in `vernac`, which is the one that really knows about constants, paving the way for further simplification and in particular for a unified handling of constant saving by removal of the control inversion here. Terminators are now internal to `Lemmas`, as it is the only part of the code applying them. As a consequence, proof nesting is now handled by `Lemmas`, and `Proof_global.t` is just a single `Proof.t` plus some environmental meta-data. We are also enable considerable simplification in a future PR, as this patch makes `Proof.t` and `Proof_global.t` essentially the same, so we should expect to handle them under a unified interface. --- plugins/ltac/rewrite.ml | 11 +++++------ plugins/ltac/rewrite.mli | 6 +++--- 2 files changed, 8 insertions(+), 9 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index b99e77ab2b..2da6584aba 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1962,7 +1962,6 @@ let add_setoid atts binders a aeq t n = (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])] - let make_tactic name = let open Tacexpr in let tacqid = Libnames.qualid_of_string name in @@ -1988,7 +1987,7 @@ let add_morphism_as_parameter atts m n : unit = (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst)); declare_projection n instance_id (ConstRef cst) -let add_morphism_interactive atts m n : Proof_global.t = +let add_morphism_interactive atts m n : Lemmas.t = warn_add_morphism_deprecated ?loc:m.CAst.loc (); init_setoid (); let instance_id = add_suffix n "_Proper" in @@ -2010,8 +2009,8 @@ let add_morphism_interactive atts m n : Proof_global.t = let hook = Lemmas.mk_hook hook in Flags.silently (fun () -> - let pstate = Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in - fst Pfedit.(by (Tacinterp.interp tac) pstate)) () + let lemma = Lemmas.start_lemma ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in + fst (Lemmas.by (Tacinterp.interp tac) lemma)) () let add_morphism atts binders m s n = init_setoid (); @@ -2023,12 +2022,12 @@ let add_morphism atts binders m s n = [cHole; s; m]) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - let _id, pstate = Classes.new_instance_interactive + let _id, lemma = Classes.new_instance_interactive ~global:atts.global atts.polymorphic instance_name binders instance_t ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info in - pstate (* no instance body -> always open proof *) + lemma (* no instance body -> always open proof *) (** Bind to "rewrite" too *) diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 3ef33c6dc9..a5c3782b30 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -101,16 +101,16 @@ val add_setoid -> Id.t -> unit -val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t +val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Lemmas.t val add_morphism_as_parameter : rewrite_attributes -> constr_expr -> Id.t -> unit val add_morphism - : rewrite_attributes + : rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t - -> Proof_global.t + -> Lemmas.t val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr -- cgit v1.2.3