[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, 13 insertions, 8 deletions

diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 490e8fbdbc..64e023c68a 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -181,13 +181,18 @@ let norwocc = noclr, None
 
 let simplintac occ rdx sim gl = 
   let simptac m gl =
-    if m <> ~-1 then
-      CErrors.user_err (Pp.str "Localized custom simpl tactic not supported");
-    let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in
-    let simp env c _ _ = EConstr.Unsafe.to_constr (red_safe Tacred.simpl env sigma0 (EConstr.of_constr c)) in
-    Proofview.V82.of_tactic
-      (convert_concl_no_check (EConstr.of_constr (eval_pattern env0 sigma0 (EConstr.Unsafe.to_constr concl0) rdx occ simp)))
-      gl in
+    if m <> ~-1 then begin
+      if rdx <> None then
+        CErrors.user_err (Pp.str "Custom simpl tactic does not support patterns");
+      if occ <> None then
+        CErrors.user_err (Pp.str "Custom simpl tactic does not support occurrence numbers");
+      simpltac (Simpl m) gl
+    end else
+      let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in
+      let simp env c _ _ = EConstr.Unsafe.to_constr (red_safe Tacred.simpl env sigma0 (EConstr.of_constr c)) in
+      Proofview.V82.of_tactic
+        (convert_concl_no_check (EConstr.of_constr (eval_pattern env0 sigma0 (EConstr.Unsafe.to_constr concl0) rdx occ simp)))
+        gl in
   match sim with
   | Simpl m -> simptac m gl
   | SimplCut (n,m) -> tclTHEN (simptac m) (tclTRY (donetac n)) gl
@@ -644,6 +649,6 @@ let unlocktac ist args gl =
   let key, gl = pf_mkSsrConst "master_key" gl in
   let ktacs = [
     (fun gl -> unfoldtac None None (project gl,locked) xInParens gl); 
-    Ssrelim.casetac key ] in
+    Proofview.V82.of_tactic (Ssrelim.casetac key (fun ?seed:_ k -> k)) ] in
   tclTHENLIST (List.map utac args @ ktacs) gl