[ssr] extended intro patterns: + > [^] /ltac:

This commit implements the following intro patterns:

Temporary "=> +"
 "move=> + stuff" ==== "move=> tmp stuff; move: tmp"
 It preserves the original name.
 "=>" can be chained to force generalization as in
 "move=> + y + => x z"

Tactics as views "=> /ltac:(tactic)"
 Supports notations, eg "Notation foo := ltac:(bla bla bla). .. => /foo".
 Limited to views on the right of "=>", views that decorate a tactic
 as move or case are not supported to be tactics.

Dependent "=> >H"
 move=> >H  ===== move=> ???? H, with enough ? to
 name H the first non-dependent assumption (LHS of the first arrow).
 TC isntances are skipped.

Block intro "=> [^ H] [^~ H]"
 after "case" or "elim" or "elim/v" it introduces in one go
 all new assumptions coming from the eliminations. The names are
 picked from the inductive type declaration or the elimination principle
 "v" in "elim/v" and are appended/prepended the seed "H"

The implementation makes crucial use of the goal_with_state feature of
the tactic monad. For example + schedules a generalization to be performed
at the end of the intro pattern and [^ .. ] reads the name seeds from
the state (that is filled in by case and elim).

1 files changed, 12 insertions, 6 deletions

diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index 8bf4816e99..6ccefa1cab 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -97,24 +97,30 @@ let pr_view2 = pr_list mt (fun c -> str "/" ++ pr_ast_closure_term c)
 
 let rec pr_ipat p =
   match p with
-  | IPatId id -> Id.print id
+  | IPatId (None,id) -> Id.print id
+  | IPatId (Some Dependent,id) -> str">" ++ Id.print id
   | IPatSimpl sim -> pr_simpl sim
   | IPatClear clr -> pr_clear mt clr
-  | IPatCase iorpat -> hov 1 (str "[" ++ pr_iorpat iorpat ++ str "]")
-  | IPatDispatch(_,iorpat) -> hov 1 (str "/[" ++ pr_iorpat iorpat ++ str "]")
+  | IPatCase (Regular iorpat) -> hov 1 (str "[" ++ pr_iorpat iorpat ++ str "]")
+  | IPatCase (Block m) -> hov 1 (str"[" ++ pr_block m ++ str"]")
+  | IPatDispatch(_,Regular iorpat) -> hov 1 (str "(" ++ pr_iorpat iorpat ++ str ")")
+  | IPatDispatch (_,Block m) -> hov 1 (str"(" ++ pr_block m ++ str")")
   | IPatInj iorpat -> hov 1 (str "[=" ++ pr_iorpat iorpat ++ str "]")
   | IPatRewrite (occ, dir) -> pr_occ occ ++ pr_dir dir
   | IPatAnon All -> str "*"
   | IPatAnon Drop -> str "_"
-  | IPatAnon One -> str "?"
+  | IPatAnon (One _) -> str "?"
   | IPatView (false,v) -> pr_view2 v
   | IPatView (true,v) -> str"{}" ++ pr_view2 v
+  | IPatAnon Temporary -> str "+"
   | IPatNoop -> str "-"
   | IPatAbstractVars l -> str "[:" ++ pr_list spc Id.print l ++ str "]"
-  | IPatTac _ -> str "<tac>"
-(* TODO  | IPatAnon Temporary -> str "+" *)
+  | IPatEqGen _ -> str "<tac>"
 and pr_ipats ipats = pr_list spc pr_ipat ipats
 and pr_iorpat iorpat = pr_list pr_bar pr_ipats iorpat
+and pr_block = function (Prefix id) -> str"^" ++ Id.print id
+                      | (SuffixId id) -> str"^~" ++ Id.print id
+                      | (SuffixNum n) -> str"^~" ++ int n
 
 (* 0 cost pp function. Active only if Debug Ssreflect is Set *)
 let ppdebug_ref = ref (fun _ -> ())