[coqpp] [ltac] Adapt to removal of imperative proof state.

We add state handling to tactics.

TODO:

- [rewrite] `add_morphism_infer` creates problems as it opens a proof.
- [g_obligations] with_tac

4 files changed, 28 insertions, 8 deletions

diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli
index 8e10ec49ce..81109887ba 100644
--- a/coqpp/coqpp_ast.mli
+++ b/coqpp/coqpp_ast.mli
@@ -103,6 +103,7 @@ type classification =
 
 type vernac_rule = {
   vernac_atts : (string * string) list option;
+  vernac_state: string option;
   vernac_toks : ext_token list;
   vernac_class : code option;
   vernac_depr : bool;
diff --git a/coqpp/coqpp_lex.mll b/coqpp/coqpp_lex.mll
index c38755943a..81ba8ad98c 100644
--- a/coqpp/coqpp_lex.mll
+++ b/coqpp/coqpp_lex.mll
@@ -130,6 +130,7 @@ rule extend = parse
 | space { extend lexbuf }
 | '\"' { string lexbuf }
 | '\n' { newline lexbuf; extend lexbuf }
+| "![" { BANGBRACKET }
 | "#[" { HASHBRACKET }
 | '[' { LBRACKET }
 | ']' { RBRACKET }
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index d33eef135f..90158c3aa3 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -347,9 +347,18 @@ let print_atts_right fmt = function
     let nota = match atts with [_] -> "" | _ -> "Attributes.Notations." in
     fprintf fmt "(Attributes.parse %s%a atts)" nota aux atts
 
+let print_body_wrapper fmt r =
+  match r.vernac_state with
+  | Some "proof" ->
+    fprintf fmt "let proof = (%a) ~pstate:st.Vernacstate.proof in { st with Vernacstate.proof }" print_code r.vernac_body
+  | None ->
+    fprintf fmt "let () = %a in st" print_code r.vernac_body
+  | Some x ->
+    fatal ("unsupported state specifier: " ^ x)
+
 let print_body_fun fmt r =
-  fprintf fmt "let coqpp_body %a%a ~st = let () = %a in st in "
-    print_binders r.vernac_toks print_atts_left r.vernac_atts print_code r.vernac_body
+  fprintf fmt "let coqpp_body %a%a ~st = @[%a@] in "
+    print_binders r.vernac_toks print_atts_left r.vernac_atts print_body_wrapper r
 
 let print_body fmt r =
   fprintf fmt "@[(%afun %a~atts@ ~st@ -> coqpp_body %a%a ~st)@]"
diff --git a/coqpp/coqpp_parse.mly b/coqpp/coqpp_parse.mly
index abe52ab46b..43ba990f6a 100644
--- a/coqpp/coqpp_parse.mly
+++ b/coqpp/coqpp_parse.mly
@@ -65,7 +65,7 @@ let parse_user_entry s sep =
 %token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN DEPRECATED ARGUMENT
 %token RAW_PRINTED GLOB_PRINTED
 %token COMMAND CLASSIFIED PRINTED TYPED INTERPRETED GLOBALIZED SUBSTITUTED BY AS
-%token HASHBRACKET LBRACKET RBRACKET PIPE ARROW FUN COMMA EQUAL STAR
+%token BANGBRACKET HASHBRACKET LBRACKET RBRACKET PIPE ARROW FUN COMMA EQUAL STAR
 %token LPAREN RPAREN COLON SEMICOLON
 %token GLOBAL FIRST LAST BEFORE AFTER LEVEL LEFTA RIGHTA NONA
 %token EOF
@@ -209,13 +209,14 @@ vernac_rules:
 ;
 
 vernac_rule:
-| PIPE vernac_attributes_opt LBRACKET ext_tokens RBRACKET rule_deprecation rule_classifier ARROW CODE
+| PIPE vernac_attributes_opt vernac_state_opt LBRACKET ext_tokens RBRACKET rule_deprecation rule_classifier ARROW CODE
   { {
       vernac_atts = $2;
-      vernac_toks = $4;
-      vernac_depr = $6;
-      vernac_class= $7;
-      vernac_body = $9;
+      vernac_state= $3;
+      vernac_toks = $5;
+      vernac_depr = $7;
+      vernac_class= $8;
+      vernac_body = $10;
   } }
 ;
 
@@ -235,6 +236,14 @@ vernac_attribute:
 | qualid_or_ident { ($1, $1) }
 ;
 
+vernac_state_opt:
+| { None }
+| BANGBRACKET vernac_state RBRACKET { Some $2 }
+;
+
+vernac_state:
+| qualid_or_ident { $1 }
+
 rule_deprecation:
 | { false }
 | DEPRECATED { true }