From 1bf2a088387949c13602997d181e6f7d0f014b3f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sun, 5 May 2019 16:32:17 +0200
Subject: rewrite.ml: drop the id returned by new_instance earlier

We never use this id in rewrite.ml so don't bother threading it around.
---
 plugins/ltac/rewrite.ml | 90 +++++++++++++++++++++++++------------------------
 1 file changed, 46 insertions(+), 44 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 164bd7e118..950115146b 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1797,9 +1797,11 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
 let anew_instance ~pstate atts binders (name,t) fields =
   let program_mode = atts.program in
-  new_instance ~pstate ~program_mode atts.polymorphic
-    name binders t (Some (true, CAst.make @@ CRecord (fields)))
-    ~global:atts.global ~generalize:false Hints.empty_hint_info
+  let _id, pstate = new_instance ~pstate ~program_mode atts.polymorphic
+      name binders t (Some (true, CAst.make @@ CRecord (fields)))
+      ~global:atts.global ~generalize:false Hints.empty_hint_info
+  in
+  pstate
 
 let declare_instance_refl ~pstate atts binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
@@ -1819,41 +1821,41 @@ let declare_instance_trans atts binders a aeq n lemma =
 let declare_relation ~pstate atts ?(binders=[]) a aeq n refl symm trans =
   init_setoid ();
   let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" in
-  let _, pstate = anew_instance ~pstate atts binders instance [] in
+  let pstate = anew_instance ~pstate atts binders instance [] in
   match (refl,symm,trans) with
-      (None, None, None) -> pstate
-    | (Some lemma1, None, None) ->
-      snd @@ declare_instance_refl ~pstate atts binders a aeq n lemma1
-    | (None, Some lemma2, None) ->
-      snd @@ declare_instance_sym ~pstate atts binders a aeq n lemma2
-    | (None, None, Some lemma3) ->
-      snd @@ declare_instance_trans ~pstate atts binders a aeq n lemma3
-    | (Some lemma1, Some lemma2, None) ->
-      let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in
-      snd @@ declare_instance_sym ~pstate atts binders a aeq n lemma2
-    | (Some lemma1, None, Some lemma3) ->
-        let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in
-        let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in
-        let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in
-        snd @@ anew_instance ~pstate atts binders instance
-              [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1);
-               (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)]
-    | (None, Some lemma2, Some lemma3) ->
-        let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in
-        let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in
-        let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in
-        snd @@ anew_instance ~pstate atts binders instance
-              [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2);
-               (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)]
-     | (Some lemma1, Some lemma2, Some lemma3) ->
-        let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in
-        let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in
-        let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in
-        let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in
-        snd @@ anew_instance ~pstate atts binders instance
-            [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1);
-             (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2);
-             (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)]
+    (None, None, None) -> pstate
+  | (Some lemma1, None, None) ->
+    declare_instance_refl ~pstate atts binders a aeq n lemma1
+  | (None, Some lemma2, None) ->
+    declare_instance_sym ~pstate atts binders a aeq n lemma2
+  | (None, None, Some lemma3) ->
+    declare_instance_trans ~pstate atts binders a aeq n lemma3
+  | (Some lemma1, Some lemma2, None) ->
+    let pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in
+    declare_instance_sym ~pstate atts binders a aeq n lemma2
+  | (Some lemma1, None, Some lemma3) ->
+    let pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in
+    let pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in
+    let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in
+    anew_instance ~pstate atts binders instance
+      [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1);
+       (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)]
+  | (None, Some lemma2, Some lemma3) ->
+    let pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in
+    let pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in
+    let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in
+    anew_instance ~pstate atts binders instance
+      [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2);
+       (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)]
+  | (Some lemma1, Some lemma2, Some lemma3) ->
+    let pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in
+    let pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in
+    let pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in
+    let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in
+    anew_instance ~pstate atts binders instance
+      [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1);
+       (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2);
+       (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)]
 
 let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None)
 
@@ -1952,15 +1954,15 @@ let warn_add_setoid_deprecated =
 let add_setoid ~pstate atts binders a aeq t n =
   warn_add_setoid_deprecated ?loc:a.CAst.loc ();
   init_setoid ();
-  let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
-  let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
-  let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
+  let pstate = declare_instance_refl ~pstate atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
+  let pstate = declare_instance_sym ~pstate atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
+  let pstate = declare_instance_trans ~pstate atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
   let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
   in
-  snd @@ anew_instance ~pstate atts binders instance
-      [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
-       (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])]
+  anew_instance ~pstate atts binders instance
+    [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
+     (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 =
-- 
cgit v1.2.3


From 1c228b648cb1755cad3ec1f38690110d6fe14bc5 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sun, 5 May 2019 16:58:10 +0200
Subject: rewrite.ml: remove outdated comment

---
 plugins/ltac/rewrite.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 950115146b..6f84e6c18d 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1977,7 +1977,6 @@ let warn_add_morphism_deprecated =
 let add_morphism_infer ~pstate atts m n : Proof_global.t option =
   warn_add_morphism_deprecated ?loc:m.CAst.loc ();
   init_setoid ();
-  (* NB: atts.program is ignored, program mode automatically set by vernacentries *)
   let instance_id = add_suffix n "_Proper" in
   let env = Global.env () in
   let evd = Evd.from_env env in
-- 
cgit v1.2.3


From 8abacf00c6c39ec98085d531737d18edc9c19b2a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 2 May 2019 19:46:02 +0200
Subject: Proof_global: pass only 1 pstate when we don't want the proof stack

Typically instead of [start_proof : ontop:Proof_global.t option -> bla ->
Proof_global.t] we have [start_proof : bla -> Proof_global.pstate] and
the pstate is pushed on the stack by a caller around the
vernacentries/mlg level.

Naming can be a bit awkward, hopefully it can be improved (maybe in a
followup PR).

We can see some patterns appear waiting for nicer combinators, eg in
mlg we often only want to work with the current proof, not the stack.

Behaviour should be similar modulo bugs, let's see what CI says.
---
 plugins/ltac/extratactics.mlg  | 2 +-
 plugins/ltac/g_obligations.mlg | 4 ++--
 plugins/ltac/g_rewrite.mlg     | 3 ++-
 plugins/ltac/rewrite.ml        | 6 +++---
 plugins/ltac/rewrite.mli       | 2 +-
 5 files changed, 9 insertions(+), 8 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 4c186dce09..5e4969567d 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -1118,7 +1118,7 @@ END
 
 VERNAC COMMAND EXTEND OptimizeProof
 | ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } ->
-  { fun ~pstate -> Option.map Proof_global.compact_the_proof pstate }
+  { fun ~pstate -> Option.map Proof_global.(modify_current_pstate compact_the_proof) pstate }
 | [ "Optimize" "Heap" ] => { classify_as_proofstep } ->
   { Gc.compact () }
 END
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index de3a9c9fa9..d7918a58ac 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -80,8 +80,8 @@ GRAMMAR EXTEND Gram
 
 open Obligations
 
-let obligation ~pstate obl tac = Some (with_tac (fun t -> Obligations.obligation ~ontop:pstate obl t) tac)
-let next_obligation ~pstate obl tac = Some (with_tac (fun t -> Obligations.next_obligation ~ontop:pstate obl t) tac)
+let obligation ~pstate obl tac = Some (Proof_global.push ~ontop:pstate (with_tac (fun t -> Obligations.obligation obl t) tac))
+let next_obligation ~pstate obl tac = Some (Proof_global.push ~ontop:pstate (with_tac (fun t -> Obligations.next_obligation obl t) tac))
 
 let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater)
 
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 2fad1f6b6a..e3f4b8ef59 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -280,7 +280,8 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
     (* This command may or may not open a goal *)
     => { (if Lib.is_modtype() then VtSideff([n]) else VtStartProof(GuaranteesOpacity, [n])), VtLater }
     -> {
-          add_morphism_infer atts m n
+      fun ~pstate:ontop ->
+        Option.cata (fun ps -> Some (Proof_global.push ~ontop ps)) ontop (add_morphism_infer atts m n)
        }
   | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
     => { VtStartProof(GuaranteesOpacity,[n]), VtLater }
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 6f84e6c18d..efca411754 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1974,7 +1974,7 @@ let warn_add_morphism_deprecated =
   CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () ->
       Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id"))
 
-let add_morphism_infer ~pstate atts m n : Proof_global.t option =
+let add_morphism_infer atts m n : Proof_global.pstate option =
   warn_add_morphism_deprecated ?loc:m.CAst.loc ();
   init_setoid ();
   let instance_id = add_suffix n "_Proper" in
@@ -1991,7 +1991,7 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option =
       add_instance (Classes.mk_instance
                       (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst));
       declare_projection n instance_id (ConstRef cst);
-      pstate
+      None
     else
       let kind = Decl_kinds.Global, atts.polymorphic,
                  Decl_kinds.DefinitionBody Decl_kinds.Instance
@@ -2008,7 +2008,7 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option =
       let hook = Lemmas.mk_hook hook in
       Flags.silently
         (fun () ->
-           let pstate = Lemmas.start_proof ~ontop:pstate ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
+           let pstate = Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
            Some (fst Pfedit.(by (Tacinterp.interp tac) pstate))) ()
 
 let add_morphism ~pstate atts binders m s n =
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index a200cb5ced..cab7d0065e 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -89,7 +89,7 @@ val add_setoid : pstate:Proof_global.t option ->
   rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr ->
   Id.t -> Proof_global.t option
 
-val add_morphism_infer : pstate:Proof_global.t option -> rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t option
+val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.pstate option
 
 val add_morphism : pstate:Proof_global.t option ->
   rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> Proof_global.t option
-- 
cgit v1.2.3


From b8842c3c8d6e6d9d4c19a75453fca9f94de6fa49 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 3 May 2019 14:14:40 +0200
Subject: coqpp: add new ![] specifiers for structured proof interaction

![proof_stack] is equivalent to the old meaning of ![proof]: the body
has type `pstate:Proof_global.t option -> Proof_global.t option`

The other specifiers are for the following body types:

~~~
![open_proof] `is_ontop:bool -> pstate`

![maybe_open_proof] `is_ontop:bool -> pstate option`

![proof] `pstate:pstate -> pstate`

![proof_opt_query] `pstate:pstate option -> unit`

![proof_query] `pstate:pstate -> unit`
~~~

The `is_ontop` is only used for the warning message when declaring a
section variable inside a proof, we could also just stop warning.

The specifiers look closely related to stm classifiers, but currently
they're unconnected. Notably this means that a ![proof_query] doesn't
have to be classified QUERY.

![proof_stack] is only used by g_rewrite/rewrite whose behaviour I
 don't fully understand, maybe we can drop it in the future.

For compat we may want to consider keeping ![proof] with its old
meaning and using some new name for the new meaning. OTOH fixing
plugins to be stricter is easier if we change it as the errors tell us
where it's used.
---
 plugins/ltac/extratactics.mlg  |  6 ++--
 plugins/ltac/g_ltac.mlg        |  8 ++---
 plugins/ltac/g_obligations.mlg | 16 +++++-----
 plugins/ltac/g_rewrite.mlg     | 55 +++++++++++++++-------------------
 plugins/ltac/rewrite.ml        | 67 +++++++++++++++++++++---------------------
 plugins/ltac/rewrite.mli       | 35 ++++++++++++++++------
 6 files changed, 98 insertions(+), 89 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 5e4969567d..4a2fb425ac 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -934,7 +934,7 @@ END
 VERNAC COMMAND EXTEND GrabEvars
 | ![ proof ] [ "Grab" "Existential" "Variables" ]
   => { classify_as_proofstep }
-  -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p  -> Proof.V82.grab_evars p)) pstate }
+  -> { fun ~pstate -> Proof_global.modify_proof (fun p  -> Proof.V82.grab_evars p) pstate }
 END
 
 (* Shelves all the goals under focus. *)
@@ -966,7 +966,7 @@ END
 VERNAC COMMAND EXTEND Unshelve
 | ![ proof ] [ "Unshelve" ]
   => { classify_as_proofstep }
-  -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p  -> Proof.unshelve p)) pstate  }
+  -> { fun ~pstate -> Proof_global.modify_proof (fun p  -> Proof.unshelve p) pstate  }
 END
 
 (* Gives up on the goals under focus: the goals are considered solved,
@@ -1118,7 +1118,7 @@ END
 
 VERNAC COMMAND EXTEND OptimizeProof
 | ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } ->
-  { fun ~pstate -> Option.map Proof_global.(modify_current_pstate compact_the_proof) pstate }
+  { fun ~pstate -> Proof_global.compact_the_proof pstate }
 | [ "Optimize" "Heap" ] => { classify_as_proofstep } ->
   { Gc.compact () }
 END
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 7eb34158e8..9bf5bd1bda 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -376,7 +376,7 @@ let () = declare_int_option {
 
 let vernac_solve ~pstate n info tcom b =
   let open Goal_select in
-  let pstate, status = Proof_global.with_current_proof (fun etac p ->
+  let pstate, status = Proof_global.with_proof (fun etac p ->
       let with_end_tac = if b then Some etac else None in
       let global = match n with SelectAll | SelectList _ -> true | _ -> false in
       let info = Option.append info !print_info_trace in
@@ -388,7 +388,7 @@ let vernac_solve ~pstate n info tcom b =
       let p = Proof.maximal_unfocus Vernacentries.command_focus p in
       p,status) pstate in
   if not status then Feedback.feedback Feedback.AddedAxiom;
-  Some pstate
+  pstate
 
 let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s
 
@@ -438,7 +438,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve
 | ![ proof ] [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
     { classify_as_proofstep } -> {
     let g = Option.default (Goal_select.get_default_goal_selector ()) g in
-    Vernacentries.vernac_require_open_proof vernac_solve g n t def
+    vernac_solve g n t def
   }
 | ![ proof ] [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
     {
@@ -450,7 +450,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve
       VtLater
     } -> {
       let t = rm_abstract t in
-      Vernacentries.vernac_require_open_proof vernac_solve Goal_select.SelectAll n t def
+      vernac_solve Goal_select.SelectAll n t def
     }
 END
 
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index d7918a58ac..c01b97c14d 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -80,25 +80,25 @@ GRAMMAR EXTEND Gram
 
 open Obligations
 
-let obligation ~pstate obl tac = Some (Proof_global.push ~ontop:pstate (with_tac (fun t -> Obligations.obligation obl t) tac))
-let next_obligation ~pstate obl tac = Some (Proof_global.push ~ontop:pstate (with_tac (fun t -> Obligations.next_obligation obl t) tac))
+let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac
+let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac
 
 let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater)
 
 }
 
 VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl }
-| ![ proof ] [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
+| ![ open_proof ] [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
     { obligation (num, Some name, Some t) tac }
-| ![ proof ] [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
+| ![ open_proof ] [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
     { obligation (num, Some name, None) tac }
-| ![ proof ] [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
+| ![ open_proof ] [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
     { obligation (num, None, Some t) tac }
-| ![ proof ] [ "Obligation" integer(num) withtac(tac) ] ->
+| ![ open_proof ] [ "Obligation" integer(num) withtac(tac) ] ->
     { obligation (num, None, None) tac }
-| ![ proof ] [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
+| ![ open_proof ] [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
     { next_obligation (Some name) tac }
-| ![ proof ] [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac }
+| ![ open_proof ] [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac }
 END
 
 VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index e3f4b8ef59..bb29323858 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -180,34 +180,34 @@ TACTIC EXTEND setoid_rewrite
 END
 
 VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
         "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
       { declare_relation atts a aeq n (Some lemma1) (Some lemma2) None }
 
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
         "as" ident(n) ] ->
       { declare_relation atts a aeq n (Some lemma1) None None }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq)  "as" ident(n) ] ->
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq)  "as" ident(n) ] ->
       { declare_relation atts a aeq n None None None }
 END
 
 VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
       "as" ident(n) ] ->
       { declare_relation atts a aeq n None (Some lemma2) None }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
       { declare_relation atts a aeq n None (Some lemma2) (Some lemma3) }
 END
 
 VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
       { declare_relation atts a aeq n (Some lemma1) None (Some lemma3) }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
       "as" ident(n) ] ->
       { declare_relation atts a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
         "as" ident(n) ] ->
       { declare_relation atts a aeq n None None (Some lemma3) }
 END
@@ -234,66 +234,59 @@ GRAMMAR EXTEND Gram
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
         "reflexivity" "proved" "by" constr(lemma1)
         "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) None }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
         "reflexivity" "proved" "by" constr(lemma1)
         "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n (Some lemma1) None None }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)  "as" ident(n) ] ->
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)  "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n None None None }
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
       "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n None (Some lemma2) None }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n None (Some lemma2) (Some lemma3) }
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n (Some lemma1) None (Some lemma3) }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
       "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
         "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n None None (Some lemma3) }
 END
 
 VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+  | #[ atts = rewrite_attributes; ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
      {
          add_setoid atts [] a aeq t n
      }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
      {
          add_setoid atts binders a aeq t n
      }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
+  | #[ atts = rewrite_attributes; ] ![ maybe_open_proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
     (* This command may or may not open a goal *)
     => { (if Lib.is_modtype() then VtSideff([n]) else VtStartProof(GuaranteesOpacity, [n])), VtLater }
-    -> {
-      fun ~pstate:ontop ->
-        Option.cata (fun ps -> Some (Proof_global.push ~ontop ps)) ontop (add_morphism_infer atts m n)
-       }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
+    -> { add_morphism_infer atts m n }
+  | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
     => { VtStartProof(GuaranteesOpacity,[n]), VtLater }
-    -> {
-          add_morphism atts [] m s n
-       }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
+    -> { add_morphism atts [] m s n }
+  | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
         "with" "signature" lconstr(s) "as" ident(n) ]
     => { VtStartProof(GuaranteesOpacity,[n]), VtLater }
-    -> {
-          add_morphism atts binders m s n
-       }
+    -> { add_morphism atts binders m s n }
 END
 
 TACTIC EXTEND setoid_symmetry
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index efca411754..5d57a2f27f 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -23,7 +23,6 @@ open Tacticals.New
 open Tactics
 open Pretype_errors
 open Typeclasses
-open Classes
 open Constrexpr
 open Globnames
 open Evd
@@ -1795,17 +1794,17 @@ let declare_an_instance n s args =
 
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
-let anew_instance ~pstate atts binders (name,t) fields =
+let anew_instance atts binders (name,t) fields =
   let program_mode = atts.program in
-  let _id, pstate = new_instance ~pstate ~program_mode atts.polymorphic
+  let _id, proof = Classes.new_instance ~program_mode atts.polymorphic
       name binders t (Some (true, CAst.make @@ CRecord (fields)))
       ~global:atts.global ~generalize:false Hints.empty_hint_info
   in
-  pstate
+  assert (Option.is_empty proof) (* refine:false with term *)
 
-let declare_instance_refl ~pstate atts binders a aeq n lemma =
+let declare_instance_refl atts binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
-  in anew_instance ~pstate atts binders instance
+  in anew_instance atts binders instance
        [(qualid_of_ident (Id.of_string "reflexivity"),lemma)]
 
 let declare_instance_sym atts binders a aeq n lemma =
@@ -1818,41 +1817,41 @@ let declare_instance_trans atts binders a aeq n lemma =
   in anew_instance atts binders instance
        [(qualid_of_ident (Id.of_string "transitivity"),lemma)]
 
-let declare_relation ~pstate atts ?(binders=[]) a aeq n refl symm trans =
+let declare_relation atts ?(binders=[]) a aeq n refl symm trans =
   init_setoid ();
   let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" in
-  let pstate = anew_instance ~pstate atts binders instance [] in
+  let () = anew_instance atts binders instance [] in
   match (refl,symm,trans) with
-    (None, None, None) -> pstate
+    (None, None, None) -> ()
   | (Some lemma1, None, None) ->
-    declare_instance_refl ~pstate atts binders a aeq n lemma1
+    declare_instance_refl atts binders a aeq n lemma1
   | (None, Some lemma2, None) ->
-    declare_instance_sym ~pstate atts binders a aeq n lemma2
+    declare_instance_sym atts binders a aeq n lemma2
   | (None, None, Some lemma3) ->
-    declare_instance_trans ~pstate atts binders a aeq n lemma3
+    declare_instance_trans atts binders a aeq n lemma3
   | (Some lemma1, Some lemma2, None) ->
-    let pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in
-    declare_instance_sym ~pstate atts binders a aeq n lemma2
+    let () = declare_instance_refl atts binders a aeq n lemma1 in
+    declare_instance_sym atts binders a aeq n lemma2
   | (Some lemma1, None, Some lemma3) ->
-    let pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in
-    let pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in
+    let () = declare_instance_refl atts binders a aeq n lemma1 in
+    let () = declare_instance_trans atts binders a aeq n lemma3 in
     let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in
-    anew_instance ~pstate atts binders instance
+    anew_instance atts binders instance
       [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1);
        (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)]
   | (None, Some lemma2, Some lemma3) ->
-    let pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in
-    let pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in
+    let () = declare_instance_sym atts binders a aeq n lemma2 in
+    let () = declare_instance_trans atts binders a aeq n lemma3 in
     let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in
-    anew_instance ~pstate atts binders instance
+    anew_instance atts binders instance
       [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2);
        (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)]
   | (Some lemma1, Some lemma2, Some lemma3) ->
-    let pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in
-    let pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in
-    let pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in
+    let () = declare_instance_refl atts binders a aeq n lemma1 in
+    let () = declare_instance_sym atts binders a aeq n lemma2 in
+    let () = declare_instance_trans atts binders a aeq n lemma3 in
     let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in
-    anew_instance ~pstate atts binders instance
+    anew_instance atts binders instance
       [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1);
        (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2);
        (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)]
@@ -1951,15 +1950,15 @@ let warn_add_setoid_deprecated =
   CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () ->
       Pp.(str "Add Setoid is deprecated, please use Add Parametric Relation."))
 
-let add_setoid ~pstate atts binders a aeq t n =
+let add_setoid atts binders a aeq t n =
   warn_add_setoid_deprecated ?loc:a.CAst.loc ();
   init_setoid ();
-  let pstate = declare_instance_refl ~pstate atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
-  let pstate = declare_instance_sym ~pstate atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
-  let pstate = declare_instance_trans ~pstate atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
+  let () = declare_instance_refl atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
+  let () = declare_instance_sym atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
+  let () = declare_instance_trans atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
   let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
   in
-  anew_instance ~pstate atts binders instance
+  anew_instance atts binders instance
     [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
      (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])]
@@ -1988,7 +1987,7 @@ let add_morphism_infer atts m n : Proof_global.pstate option =
              (None,(instance,uctx),None),
            Decl_kinds.IsAssumption Decl_kinds.Logical)
       in
-      add_instance (Classes.mk_instance
+      Classes.add_instance (Classes.mk_instance
                       (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst));
       declare_projection n instance_id (ConstRef cst);
       None
@@ -1999,7 +1998,7 @@ let add_morphism_infer atts m n : Proof_global.pstate option =
       let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
       let hook _ _ _ = function
         | Globnames.ConstRef cst ->
-          add_instance (Classes.mk_instance
+          Classes.add_instance (Classes.mk_instance
                           (PropGlobal.proper_class env evd) Hints.empty_hint_info
                           atts.global (ConstRef cst));
           declare_projection n instance_id (ConstRef cst)
@@ -2011,7 +2010,7 @@ let add_morphism_infer atts m n : Proof_global.pstate option =
            let pstate = Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
            Some (fst Pfedit.(by (Tacinterp.interp tac) pstate))) ()
 
-let add_morphism ~pstate atts binders m s n =
+let add_morphism atts binders m s n =
   init_setoid ();
   let instance_id = add_suffix n "_Proper" in
   let instance_name = (CAst.make @@ Name instance_id),None in
@@ -2021,12 +2020,12 @@ let add_morphism ~pstate atts binders m s n =
        [cHole; s; m])
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
-  let _, pstate = new_instance ~pstate
+  let _, pstate = Classes.new_instance
       ~program_mode:atts.program ~global:atts.global atts.polymorphic
       instance_name binders instance_t None
       ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info
   in
-  pstate
+  Option.get pstate (* no instance body -> always open proof *)
 
 (** Bind to "rewrite" too *)
 
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index cab7d0065e..e1cbc46b3b 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -81,18 +81,35 @@ val cl_rewrite_clause :
 val is_applied_rewrite_relation :
   env -> evar_map -> rel_context -> constr -> types option
 
-val declare_relation : pstate:Proof_global.t option -> rewrite_attributes ->
-  ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t ->
-  constr_expr option -> constr_expr option -> constr_expr option -> Proof_global.t option
-
-val add_setoid : pstate:Proof_global.t option ->
-  rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr ->
-  Id.t -> Proof_global.t option
+val declare_relation
+  : rewrite_attributes
+  -> ?binders:local_binder_expr list
+  -> constr_expr
+  -> constr_expr
+  -> Id.t
+  -> constr_expr option
+  -> constr_expr option
+  -> constr_expr option
+  -> unit
+
+val add_setoid
+  : rewrite_attributes
+  -> local_binder_expr list
+  -> constr_expr
+  -> constr_expr
+  -> constr_expr
+  -> Id.t
+  -> unit
 
 val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.pstate option
 
-val add_morphism : pstate:Proof_global.t option ->
-  rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> Proof_global.t option
+val add_morphism
+  : rewrite_attributes
+  -> local_binder_expr list
+  -> constr_expr
+  -> constr_expr
+  -> Id.t
+  -> Proof_global.pstate
 
 val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr
 
-- 
cgit v1.2.3


From 02fda88fc065577f3f9604477db2e03eb4d5a9b4 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 7 May 2019 14:34:06 +0200
Subject: Alternate syntax for ![]: VERNAC EXTEND Foo STATE proof

eg ![proof] becomes STATE proof

This commits still supports the old ![]
so there is redundancy:
~~~
VERNAC EXTEND Foo STATE proof
| ...

VERNAC EXTEND Foo
| ![proof] ...
~~~
with the ![] form being local to the rule and the STATE form
applying to the whole EXTEND except for the rules with a ![].
---
 plugins/ltac/extratactics.mlg  |  8 ++++----
 plugins/ltac/g_ltac.mlg        |  6 +++---
 plugins/ltac/g_obligations.mlg | 14 +++++++-------
 3 files changed, 14 insertions(+), 14 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 4a2fb425ac..0ded60d9c7 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -931,8 +931,8 @@ END
 (* spiwack: I put it in extratactics because it is somewhat tied with
    the semantics of the LCF-style tactics, hence with the classic tactic
    mode. *)
-VERNAC COMMAND EXTEND GrabEvars
-| ![ proof ] [ "Grab" "Existential" "Variables" ]
+VERNAC COMMAND EXTEND GrabEvars STATE proof
+| [ "Grab" "Existential" "Variables" ]
   => { classify_as_proofstep }
   -> { fun ~pstate -> Proof_global.modify_proof (fun p  -> Proof.V82.grab_evars p) pstate }
 END
@@ -963,8 +963,8 @@ TACTIC EXTEND unshelve
 END
 
 (* Command to add every unshelved variables to the focus *)
-VERNAC COMMAND EXTEND Unshelve
-| ![ proof ] [ "Unshelve" ]
+VERNAC COMMAND EXTEND Unshelve STATE proof
+| [ "Unshelve" ]
   => { classify_as_proofstep }
   -> { fun ~pstate -> Proof_global.modify_proof (fun p  -> Proof.unshelve p) pstate  }
 END
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 9bf5bd1bda..960e5b76f8 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -434,13 +434,13 @@ let is_explicit_terminator = function TacSolve _ -> true | _ -> false
 
 }
 
-VERNAC { tactic_mode } EXTEND VernacSolve
-| ![ proof ] [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+VERNAC { tactic_mode } EXTEND VernacSolve STATE proof
+| [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
     { classify_as_proofstep } -> {
     let g = Option.default (Goal_select.get_default_goal_selector ()) g in
     vernac_solve g n t def
   }
-| ![ proof ] [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+| [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
     {
       let anon_abstracting_tac = is_anonymous_abstract t in
       let solving_tac = is_explicit_terminator t in
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index c01b97c14d..58c8dabd79 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -87,18 +87,18 @@ let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), V
 
 }
 
-VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl }
-| ![ open_proof ] [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
+VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE open_proof
+| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
     { obligation (num, Some name, Some t) tac }
-| ![ open_proof ] [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
+| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
     { obligation (num, Some name, None) tac }
-| ![ open_proof ] [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
+| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
     { obligation (num, None, Some t) tac }
-| ![ open_proof ] [ "Obligation" integer(num) withtac(tac) ] ->
+| [ "Obligation" integer(num) withtac(tac) ] ->
     { obligation (num, None, None) tac }
-| ![ open_proof ] [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
+| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
     { next_obligation (Some name) tac }
-| ![ open_proof ] [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac }
+| [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac }
 END
 
 VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF
-- 
cgit v1.2.3


From 99154fcb97653c606d2e62e0a0521c4afddff44c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 20 May 2019 17:11:00 +0200
Subject: Rename Proof_global.{pstate -> t}

---
 plugins/ltac/rewrite.ml  | 2 +-
 plugins/ltac/rewrite.mli | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 5d57a2f27f..26d477fee0 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1973,7 +1973,7 @@ let warn_add_morphism_deprecated =
   CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () ->
       Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id"))
 
-let add_morphism_infer atts m n : Proof_global.pstate option =
+let add_morphism_infer atts m n : Proof_global.t option =
   warn_add_morphism_deprecated ?loc:m.CAst.loc ();
   init_setoid ();
   let instance_id = add_suffix n "_Proper" in
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index e1cbc46b3b..5aabb946d5 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -101,7 +101,7 @@ val add_setoid
   -> Id.t
   -> unit
 
-val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.pstate option
+val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t option
 
 val add_morphism
   : rewrite_attributes
@@ -109,7 +109,7 @@ val add_morphism
   -> constr_expr
   -> constr_expr
   -> Id.t
-  -> Proof_global.pstate
+  -> Proof_global.t
 
 val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr
 
-- 
cgit v1.2.3


From 2ebd73901edb94030aa804572cbe86d486ca6732 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 May 2019 17:50:44 +0200
Subject: [rewrite] Add Morphism syntax made different for module type
 parameters

---
 plugins/ltac/g_rewrite.mlg | 12 ++++++---
 plugins/ltac/rewrite.ml    | 62 ++++++++++++++++++++++++----------------------
 plugins/ltac/rewrite.mli   |  3 ++-
 3 files changed, 43 insertions(+), 34 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index bb29323858..1a84158df7 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -276,10 +276,14 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
      {
          add_setoid atts binders a aeq t n
      }
-  | #[ atts = rewrite_attributes; ] ![ maybe_open_proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
-    (* This command may or may not open a goal *)
-    => { (if Lib.is_modtype() then VtSideff([n]) else VtStartProof(GuaranteesOpacity, [n])), VtLater }
-    -> { add_morphism_infer atts m n }
+  | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
+    => { VtStartProof(GuaranteesOpacity, [n]), VtLater }
+    -> { if Lib.is_modtype () then
+           CErrors.user_err Pp.(str "Add Morphism cannot be used in a module type. Use Parameter Morphism instead.");
+         add_morphism_interactive atts m n }
+  | #[ atts = rewrite_attributes; ] [ "Declare" "Morphism" constr(m) ":" ident(n) ]
+    => { VtSideff([n]), VtLater }
+    -> { add_morphism_as_parameter atts m n }
   | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
     => { VtStartProof(GuaranteesOpacity,[n]), VtLater }
     -> { add_morphism atts [] m s n }
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 26d477fee0..c568f63903 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1973,42 +1973,46 @@ let warn_add_morphism_deprecated =
   CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () ->
       Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id"))
 
-let add_morphism_infer atts m n : Proof_global.t option =
+let add_morphism_as_parameter atts m n : unit =
+  init_setoid ();
+  let instance_id = add_suffix n "_Proper" in
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+  let uctx, instance = build_morphism_signature env evd m in
+  let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in
+  let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
+      (Entries.ParameterEntry
+         (None,(instance,uctx),None),
+       Decl_kinds.IsAssumption Decl_kinds.Logical)
+  in
+  Classes.add_instance (Classes.mk_instance
+                  (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 =
   warn_add_morphism_deprecated ?loc:m.CAst.loc ();
   init_setoid ();
   let instance_id = add_suffix n "_Proper" in
   let env = Global.env () in
   let evd = Evd.from_env env in
   let uctx, instance = build_morphism_signature env evd m in
-    if Lib.is_modtype () then
-      let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in
-      let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
-          (Entries.ParameterEntry
-             (None,(instance,uctx),None),
-           Decl_kinds.IsAssumption Decl_kinds.Logical)
-      in
+  let kind = Decl_kinds.Global, atts.polymorphic,
+             Decl_kinds.DefinitionBody Decl_kinds.Instance
+  in
+  let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
+  let hook _ _ _ = function
+    | Globnames.ConstRef cst ->
       Classes.add_instance (Classes.mk_instance
-                      (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst));
-      declare_projection n instance_id (ConstRef cst);
-      None
-    else
-      let kind = Decl_kinds.Global, atts.polymorphic,
-                 Decl_kinds.DefinitionBody Decl_kinds.Instance
-      in
-      let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
-      let hook _ _ _ = function
-        | Globnames.ConstRef cst ->
-          Classes.add_instance (Classes.mk_instance
-                          (PropGlobal.proper_class env evd) Hints.empty_hint_info
-                          atts.global (ConstRef cst));
-          declare_projection n instance_id (ConstRef cst)
-        | _ -> assert false
-      in
-      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
-           Some (fst Pfedit.(by (Tacinterp.interp tac) pstate))) ()
+                      (PropGlobal.proper_class env evd) Hints.empty_hint_info
+                      atts.global (ConstRef cst));
+      declare_projection n instance_id (ConstRef cst)
+    | _ -> assert false
+  in
+  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 add_morphism atts binders m s n =
   init_setoid ();
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 5aabb946d5..3ef33c6dc9 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -101,7 +101,8 @@ val add_setoid
   -> Id.t
   -> unit
 
-val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t option
+val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t
+val add_morphism_as_parameter : rewrite_attributes -> constr_expr -> Id.t -> unit
 
 val add_morphism
   : rewrite_attributes
-- 
cgit v1.2.3


From a7a6fa3219134004f1fc6c757f1c16281724f38f Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 24 May 2019 14:57:33 +0200
Subject: [vernac] more precise types for Add Morph, Instance, and Function

---
 plugins/ltac/rewrite.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index c568f63903..caeedadbf4 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1796,11 +1796,11 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
 let anew_instance atts binders (name,t) fields =
   let program_mode = atts.program in
-  let _id, proof = Classes.new_instance ~program_mode atts.polymorphic
-      name binders t (Some (true, CAst.make @@ CRecord (fields)))
+  let _id = Classes.new_instance ~program_mode atts.polymorphic
+      name binders t (true, CAst.make @@ CRecord (fields))
       ~global:atts.global ~generalize:false Hints.empty_hint_info
   in
-  assert (Option.is_empty proof) (* refine:false with term *)
+  ()
 
 let declare_instance_refl atts binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
@@ -2024,12 +2024,12 @@ let add_morphism atts binders m s n =
        [cHole; s; m])
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
-  let _, pstate = Classes.new_instance
+  let _id, pstate = Classes.new_instance_interactive
       ~program_mode:atts.program ~global:atts.global atts.polymorphic
-      instance_name binders instance_t None
+      instance_name binders instance_t
       ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info
   in
-  Option.get pstate (* no instance body -> always open proof *)
+  pstate (* no instance body -> always open proof *)
 
 (** Bind to "rewrite" too *)
 
-- 
cgit v1.2.3


From 06df92fffc05d501fefdcf949625a33bd52f1980 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 27 May 2019 15:53:50 +0200
Subject: [classes] remove program mode from the new_instance_* APIs

---
 plugins/ltac/rewrite.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index caeedadbf4..792cd5f9ef 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1795,8 +1795,7 @@ let declare_an_instance n s args =
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
 let anew_instance atts binders (name,t) fields =
-  let program_mode = atts.program in
-  let _id = Classes.new_instance ~program_mode atts.polymorphic
+  let _id = Classes.new_instance atts.polymorphic
       name binders t (true, CAst.make @@ CRecord (fields))
       ~global:atts.global ~generalize:false Hints.empty_hint_info
   in
@@ -2025,7 +2024,7 @@ let add_morphism atts binders m s n =
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
   let _id, pstate = Classes.new_instance_interactive
-      ~program_mode:atts.program ~global:atts.global atts.polymorphic
+      ~global:atts.global atts.polymorphic
       instance_name binders instance_t
       ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info
   in
-- 
cgit v1.2.3


From cfbfce0639a4e608210b21227f923a4f27ab6752 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 27 May 2019 17:11:53 +0200
Subject: [rewrite] remove program_mode from attributes (unused)

---
 plugins/ltac/rewrite.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 792cd5f9ef..7b286e69dc 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -42,13 +42,13 @@ module NamedDecl = Context.Named.Declaration
 
 (** Typeclass-based generalized rewriting. *)
 
-type rewrite_attributes = { polymorphic : bool; program : bool; global : bool }
+type rewrite_attributes = { polymorphic : bool; global : bool }
 
 let rewrite_attributes =
   let open Attributes.Notations in
   Attributes.(polymorphic ++ program ++ locality) >>= fun ((polymorphic, program), locality) ->
   let global = not (Locality.make_section_locality locality) in
-  Attributes.Notations.return { polymorphic; program; global }
+  Attributes.Notations.return { polymorphic; global }
 
 (** Constants used by the tactic. *)
 
-- 
cgit v1.2.3