[ssr] make > a stand alone intro pattern

9 files changed, 73 insertions, 37 deletions

diff --git a/CHANGES.md b/CHANGES.md
index d64b5accd7..7122b48809 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -144,7 +144,7 @@ SSReflect
 - New intro patterns:
   - temporary introduction: => +
   - block introduction: => [^ prefix ] [^~ suffix ]
-  - fast introduction: => >H
+  - fast introduction: => >
   - tactics as views: => /ltac:mytac
   See the reference manual for the actual documentation.
 
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index bffbe3e284..66338d7f9f 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -1559,7 +1559,7 @@ whose general syntax is
    i_view ::= {? %{%} } /@term %| /ltac:( @tactic )
 
 .. prodn::
-   i_pattern ::= @ident %| > @ident %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch }<- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ]
+   i_pattern ::= @ident %| > %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch }<- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ]
 
 .. prodn::
    i_block ::= [^ @ident ] %| [^~ @ident ] %| [^~ @num ]
@@ -1615,16 +1615,17 @@ annotation: views are interpreted opening the ``ssripat`` scope.
   a new constant, fact, or defined constant :token:`ident`, respectively.
   Note that defined constants cannot be introduced when δ-expansion is
   required to expose the top variable or assumption.
-``>``:token:`ident`
-  pops the first assumption. Type class instances are not considered
-  as assumptions.
-  The tactic ``move=> >H`` is equivalent to
-  ``move=> ? ? H`` with enough ``?`` to name ``H`` the first assumption.
-  On a goal::
+``>``
+  pops every variable occurring in the rest of the stack.
+  Type class instances are popped even if then don't occur
+  in the rest of the stack.
+  The tactic ``move=> >`` is equivalent to
+  ``move=> ? ?`` on a goal such as::
 
     forall x y, x < y -> G
 
-  it names ``H`` the assumption ``x < y``.
+  A typical use if ``move=>> H`` to name ``H`` the first assumption,
+  in the example above ``x < y``.
 ``?``
   pops the top variable into an anonymous constant or fact, whose name
   is picked by the tactic interpreter. |SSR| only generates names that cannot
@@ -5305,7 +5306,7 @@ discharge item see :ref:`discharge_ssr`
 
 generalization item see :ref:`structure_ssr`
 
-.. prodn:: i_pattern ::= @ident %| > @ident %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch } <- %| [ {?|  @i_item } ] %| - %| [: {+ @ident } ]
+.. prodn:: i_pattern ::= @ident %| > %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch } <- %| [ {?|  @i_item } ] %| - %| [: {+ @ident } ]
 
 intro pattern :ref:`introduction_ssr`
 
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index fac524da6b..dd2c2d0ba4 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -64,8 +64,6 @@ type ast_closure_term = {
 
 type ssrview = ast_closure_term list
 
-type id_mod = Dependent
-
 type id_block = Prefix of Id.t | SuffixId of Id.t | SuffixNum of int
 
 (* Only [One] forces an introduction, possibly reducing the goal. *)
@@ -77,7 +75,7 @@ type anon_iter =
 
 type ssripat =
   | IPatNoop
-  | IPatId of id_mod option * Id.t
+  | IPatId of Id.t
   | IPatAnon of anon_iter (* inaccessible name *)
 (* TODO  | IPatClearMark *)
   | IPatDispatch of bool (* ssr exception: accept a dispatch on the empty list even when there are subgoals *) * ssripatss_or_block (* (..|..) *)
@@ -88,6 +86,7 @@ type ssripat =
   | IPatClear of ssrclear (* {H1 H2} *)
   | IPatSimpl of ssrsimpl
   | IPatAbstractVars of Id.t list
+  | IPatFastNondep
   | IPatEqGen of unit Proofview.tactic (* internal use: generation of eqn *)
 
 and ssripats = ssripat list
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 37c583ab53..257ecd2a85 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -206,7 +206,7 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
   let mkabs gen = abs_wgen false (fun x -> x) gen in
   let mkclr gen clrs = clr_of_wgen gen clrs in
   let mkpats = function
-  | _, Some ((x, _), _) -> fun pats -> IPatId (None,hoi_id x) :: pats
+  | _, Some ((x, _), _) -> fun pats -> IPatId (hoi_id x) :: pats
   | _ -> fun x -> x in
   let ct = match Ssrcommon.ssrterm_of_ast_closure_term ct with
   | (a, (b, Some ct)) ->
@@ -265,7 +265,7 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
       if gens = [] then errorstrm(str"gen have requires some generalizations");
       let clear0 = old_cleartac clr0 in
       let id, name_general_hyp, cleanup, pats = match id, pats with
-      | None, (IPatId(_, id) as ip)::pats -> Some id, tacipat [ip], clear0, pats
+      | None, (IPatId id as ip)::pats -> Some id, tacipat [ip], clear0, pats
       | None, _ -> None, Tacticals.tclIDTAC, clear0, pats
       | Some (Some id),_ -> Some id, introid id, clear0, pats
       | Some _,_ ->
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index e71e1bae0d..ce81d83661 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -292,7 +292,7 @@ let tac_intro_seed interp_ipats fix = Goal.enter begin fun gl ->
              | Prefix fix ->  Id.to_string fix ^ Id.to_string id
              | SuffixNum n -> Id.to_string id ^ string_of_int n
              | SuffixId fix -> Id.to_string id ^ Id.to_string fix in
-           IPatId (None, Id.of_string s)) seeds in
+           IPatId (Id.of_string s)) seeds in
     interp_ipats ipats
 end end
 
@@ -377,9 +377,8 @@ let rec ipat_tac1 ipat : bool tactic =
   | IPatDispatch(_,Block id_block) ->
       tac_intro_seed ipat_tac id_block <*> notTAC
 
-  | IPatId (None, id) -> Ssrcommon.tclINTRO_ID id <*> notTAC
-  | IPatId (Some Dependent, id) ->
-      intro_anon_deps <*> Ssrcommon.tclINTRO_ID id <*> notTAC
+  | IPatId id -> Ssrcommon.tclINTRO_ID id <*> notTAC
+  | IPatFastNondep -> intro_anon_deps <*> notTAC
 
   | IPatCase (Block id_block) ->
       Ssrcommon.tclWITHTOP tac_case <*> tac_intro_seed ipat_tac id_block <*> notTAC
@@ -456,7 +455,7 @@ let elaborate_ipats l =
   | IPatDispatch(s, Regular p) :: rest -> IPatDispatch (s, Regular (List.map elab p)) :: elab rest
   | IPatCase (Regular p) :: rest -> IPatCase (Regular (List.map elab p)) :: elab rest
   | IPatInj p :: rest -> IPatInj (List.map elab p) :: elab rest
-  | (IPatEqGen _ | IPatId _ | IPatSimpl _ | IPatClear _ |
+  | (IPatEqGen _ | IPatId _ | IPatSimpl _ | IPatClear _ | IPatFastNondep |
      IPatAnon _ | IPatView _ | IPatNoop | IPatRewrite _ |
      IPatAbstractVars _ | IPatDispatch(_, Block _) | IPatCase(Block _)) as x :: rest -> x :: elab rest
   in
@@ -512,8 +511,7 @@ let mkCoqRefl t c env sigma =
 let elim_intro_tac ipats ?seed what eqid ssrelim is_rec clr =
   let intro_eq =
     match eqid with
-    | Some (IPatId (Some _, _)) -> assert false (* parser *)
-    | Some (IPatId (None,ipat)) when not is_rec ->
+    | Some (IPatId ipat) when not is_rec ->
        let rec intro_eq () = Goal.enter begin fun g ->
          let sigma, env, concl = Goal.(sigma g, env g, concl g) in
          match EConstr.kind_of_type sigma concl with
@@ -527,7 +525,7 @@ let elim_intro_tac ipats ?seed what eqid ssrelim is_rec clr =
          |_ -> Ssrcommon.errorstrm (Pp.str "Too many names in intro pattern")
        end in
        intro_eq ()
-    | Some (IPatId (None,ipat)) ->
+    | Some (IPatId ipat) ->
        let intro_lhs = Goal.enter begin fun g ->
          let sigma = Goal.sigma g in
          let elim_name = match clr, what with
@@ -860,7 +858,7 @@ let ssrabstract dgens =
      let ipats = List.map (fun (_,cp) ->
        match id_of_pattern (interp_cpattern gl0 cp None) with
        | None -> IPatAnon (One None)
-       | Some id -> IPatId (None,id))
+       | Some id -> IPatId id)
        (List.tl gens) in
      conclusion ipats
   end in
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 6938bbc9f6..76726009ac 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -605,7 +605,7 @@ let remove_loc x = x.CAst.v
 
 let ipat_of_intro_pattern p = Tactypes.(
   let rec ipat_of_intro_pattern = function
-    | IntroNaming (IntroIdentifier id) -> IPatId (None,id)
+    | IntroNaming (IntroIdentifier id) -> IPatId id
     | IntroAction IntroWildcard -> IPatAnon Drop
     | IntroAction (IntroOrAndPattern (IntroOrPattern iorpat)) ->
       IPatCase (Regular(
@@ -629,8 +629,8 @@ let ipat_of_intro_pattern p = Tactypes.(
 )
 
 let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function
-  | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop) as x -> x
-  | IPatId (m,id) -> IPatId (m,map_id id)
+  | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop | IPatFastNondep) as x -> x
+  | IPatId id -> IPatId (map_id id)
   | IPatAbstractVars l -> IPatAbstractVars (List.map map_id l)
   | IPatClear clr -> IPatClear (List.map map_ssrhyp clr)
   | IPatCase (Regular iorpat) -> IPatCase (Regular (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat))
@@ -707,7 +707,7 @@ let interp_ipat ist gl =
         end
     | x -> x in
   let rec interp = function
-  | IPatId(_, id) when ltacvar id ->
+  | IPatId id when ltacvar id ->
     ipat_of_intro_pattern (interp_introid ist gl id)
   | IPatId _ as x -> x
   | IPatClear clr ->
@@ -729,7 +729,7 @@ let interp_ipat ist gl =
      IPatAbstractVars (List.map get_intro_id (List.map (interp_introid ist gl) l))
   | IPatView (clr,l) -> IPatView (clr,List.map (fun x -> snd(interp_ast_closure_term ist
      gl x)) l)
-  | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop) as x -> x
+  | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop | IPatFastNondep) as x -> x
   | IPatEqGen _ -> assert false (*internal usage only *)
     in
   interp
@@ -751,8 +751,8 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY { pr_ssripats }
   GLOBALIZED BY { intern_ipats }
   | [ "_" ] -> { [IPatAnon Drop] }
   | [ "*" ] -> { [IPatAnon All] }
-  | [ ">" ident(id) ] -> { [IPatId(Some Dependent,id)] }
-  | [ ident(id) ] -> { [IPatId (None,id)] }
+  | [ ">" ] -> { [IPatFastNondep] }
+  | [ ident(id) ] -> { [IPatId id] }
   | [ "?" ] -> { [IPatAnon (One None)] }
   | [ "+" ] -> { [IPatAnon Temporary] }
   | [ "++" ] -> { [IPatAnon Temporary; IPatAnon Temporary] }
@@ -1492,7 +1492,7 @@ END
 {
 
 let intro_id_to_binder = List.map (function 
-  | IPatId (None,id) ->
+  | IPatId id ->
       let { CAst.loc=xloc } as x = bvar_lname (mkCVar id) in
       (FwdPose, [BFvar]),
         CAst.make @@ CLambdaN ([CLocalAssum([x], Default Explicit, mkCHole xloc)],
@@ -1502,8 +1502,8 @@ let intro_id_to_binder = List.map (function
 let binder_to_intro_id = CAst.(List.map (function
   | (FwdPose, [BFvar]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) }
   | (FwdPose, [BFdecl _]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) } ->
-      List.map (function {v=Name id} -> IPatId (None,id) | _ -> IPatAnon (One None)) ids
-  | (FwdPose, [BFdef]), { v = CLetIn ({v=Name id},_,_,_) } -> [IPatId (None,id)]
+      List.map (function {v=Name id} -> IPatId id | _ -> IPatAnon (One None)) ids
+  | (FwdPose, [BFdef]), { v = CLetIn ({v=Name id},_,_,_) } -> [IPatId id]
   | (FwdPose, [BFdef]), { v = CLetIn ({v=Anonymous},_,_,_) } -> [IPatAnon (One None)]
   | _ -> anomaly "ssrbinder is not a binder"))
 
@@ -1994,7 +1994,7 @@ let test_ssreqid = Pcoq.Entry.of_parser "test_ssreqid" accept_ssreqid
 GRAMMAR EXTEND Gram
   GLOBAL: ssreqid;
   ssreqpat: [
-    [ id = Prim.ident -> { IPatId (None,id) }
+    [ id = Prim.ident -> { IPatId id }
     | "_" -> { IPatAnon Drop }
     | "?" -> { IPatAnon (One None) }
     | "+" -> { IPatAnon Temporary }
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index 6ccefa1cab..898e03b00e 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -97,8 +97,7 @@ let pr_view2 = pr_list mt (fun c -> str "/" ++ pr_ast_closure_term c)
 
 let rec pr_ipat p =
   match p with
-  | IPatId (None,id) -> Id.print id
-  | IPatId (Some Dependent,id) -> str">" ++ Id.print id
+  | IPatId id -> Id.print id
   | IPatSimpl sim -> pr_simpl sim
   | IPatClear clr -> pr_clear mt clr
   | IPatCase (Regular iorpat) -> hov 1 (str "[" ++ pr_iorpat iorpat ++ str "]")
@@ -115,6 +114,7 @@ let rec pr_ipat p =
   | IPatAnon Temporary -> str "+"
   | IPatNoop -> str "-"
   | IPatAbstractVars l -> str "[:" ++ pr_list spc Id.print l ++ str "]"
+  | IPatFastNondep -> 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
diff --git a/test-suite/ssr/ipat_fast_any.v b/test-suite/ssr/ipat_fast_any.v
new file mode 100644
index 0000000000..a50984c7c0
--- /dev/null
+++ b/test-suite/ssr/ipat_fast_any.v
@@ -0,0 +1,21 @@
+Require Import ssreflect.
+
+Goal forall y x : nat, x = y -> x = x.
+Proof.
+move=> + > ->. match goal with |- forall y, y = y => by [] end.
+Qed.
+
+Goal forall y x : nat, le x y -> x = y.
+Proof.
+move=> > [|].
+  by [].
+match goal with |- forall a, _ <= a -> _ = S a => admit end.
+Admitted.
+
+Goal forall y x : nat, le x y -> x = y.
+Proof.
+move=> y x.
+case E: x => >.
+  admit.
+match goal with |- S _ <= y -> S _ = y => admit end.
+Admitted.
diff --git a/test-suite/ssr/ipat_fastid.v b/test-suite/ssr/ipat_fastid.v
index 8dc0c6cf0b..b0985a0d2f 100644
--- a/test-suite/ssr/ipat_fastid.v
+++ b/test-suite/ssr/ipat_fastid.v
@@ -11,6 +11,15 @@ lazymatch goal with
 end.
 Qed.
 
+Lemma simple2 :
+  forall x, 3 <= x -> forall y, odd (y+x) -> x = y -> True.
+Proof.
+move=> >; move=>x_ge_3; move=> >; move=>xy_odd.
+lazymatch goal with
+| |- ?x = ?y -> True => done
+end.
+Qed.
+
 
 Definition stuff x := 3 <= x -> forall y, odd (y+x) -> x = y -> True.
 
@@ -22,6 +31,14 @@ lazymatch goal with
 end.
 Qed.
 
+Lemma harder2 : forall x, stuff x.
+Proof.
+move=> >; move=>x_ge_3;move=> >; move=>xy_odd.
+lazymatch goal with
+| |- ?x = ?y -> True => done
+end.
+Qed.
+
 Lemma homotop : forall x : nat, forall e : x = x, e = e -> True.
 Proof.
 move=> >eq_ee.