[ssr] make > a stand alone intro pattern

5 files changed, 24 insertions, 27 deletions

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