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 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

(limited to 'plugins/ltac/rewrite.ml')

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 *)
 
-- 
cgit v1.2.3