Merge PR #9341: [ssr] uniform clear discipline

Reviewed-by: CohenCyril
Ack-by: Zimmi48
Ack-by: gares
Reviewed-by: maximedenes

11 files changed, 292 insertions, 121 deletions

diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index dd2c2d0ba4..9ce9250a43 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -67,7 +67,7 @@ type ssrview = ast_closure_term list
 type id_block = Prefix of Id.t | SuffixId of Id.t | SuffixNum of int
 
 (* Only [One] forces an introduction, possibly reducing the goal. *)
-type anon_iter =
+type anon_kind =
   | One of string option (* name hint *)
   | Drop
   | All
@@ -76,25 +76,23 @@ type anon_iter =
 type ssripat =
   | IPatNoop
   | 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 (* (..|..) *)
-  | IPatCase of (* ipats_mod option * *) ssripatss_or_block (* this is not equivalent to /case /[..|..] if there are already multiple goals *)
+  | IPatAnon of anon_kind (* inaccessible name *)
+  | IPatDispatch of ssripatss_or_block (* (..|..) *)
+  | IPatCase of ssripatss_or_block (* [..|..] *)
   | IPatInj of ssripatss
   | IPatRewrite of (*occurrence option * rewrite_pattern **) ssrocc * ssrdir
-  | IPatView of bool * ssrview (* {}/view (true if the clear is present) *)
+  | IPatView of ssrview (* /view *)
   | 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
 and ssripatss = ssripats list
 and ssripatss_or_block =
   | Block of id_block
   | Regular of ssripats list
-type ssrhpats = ((ssrclear * ssripats) * ssripats) * ssripats
+type ssrhpats = ((ssrclear option * ssripats) * ssripats) * ssripats
 type ssrhpats_wtransp = bool * ssrhpats
 
 (* tac => inpats *)
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 311d912efd..c3b9bde9b8 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -66,7 +66,7 @@ let check_hyp_exists hyps (SsrHyp(_, id)) =
   try ignore(Context.Named.lookup id hyps)
   with Not_found -> errorstrm Pp.(str"No assumption is named " ++ Id.print id)
 
-let test_hypname_exists hyps id =
+let test_hyp_exists hyps (SsrHyp(_, id)) =
   try ignore(Context.Named.lookup id hyps); true
   with Not_found -> false
 
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 51116ccd75..e642b5e788 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -29,7 +29,7 @@ val allocc : ssrocc
 val hyp_id : ssrhyp -> Id.t
 val hyps_ids : ssrhyps -> Id.t list
 val check_hyp_exists : ('a, 'b) Context.Named.pt -> ssrhyp -> unit
-val test_hypname_exists : ('a, 'b) Context.Named.pt -> Id.t -> bool
+val test_hyp_exists : ('a, 'b) Context.Named.pt -> ssrhyp -> bool
 val check_hyps_uniq : Id.t list -> ssrhyps -> unit
 val not_section_id : Id.t -> bool
 val hyp_err : ?loc:Loc.t -> string -> Id.t -> 'a
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 257ecd2a85..8c1363020a 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -94,17 +94,23 @@ let basecuttac name c gl =
 let introstac ipats = Proofview.V82.of_tactic (tclIPAT ipats)
 
 let havetac ist
-  (transp,((((clr, pats), binders), simpl), (((fk, _), t), hint)))
+  (transp,((((clr, orig_pats), binders), simpl), (((fk, _), t), hint)))
   suff namefst gl 
 =
  let concl = pf_concl gl in
+ let pats = tclCompileIPats orig_pats in
+ let binders = tclCompileIPats binders in
+ let simpl = tclCompileIPats simpl in
  let skols, pats =
-   List.partition (function IPatAbstractVars _ -> true | _ -> false) pats in
+   List.partition (function IOpAbstractVars _ -> true | _ -> false) pats in
  let itac_mkabs = introstac skols in
- let itac_c = introstac (IPatClear clr :: pats) in
+ let itac_c, clr =
+   match clr with
+   | None -> introstac pats, []
+   | Some clr -> introstac (tclCompileIPats (IPatClear clr :: orig_pats)), clr in
  let itac, id, clr = introstac pats, Tacticals.tclIDTAC, old_cleartac clr in
  let binderstac n =
-   let rec aux = function 0 -> [] | n -> IPatAnon (One None) :: aux (n-1) in
+   let rec aux = function 0 -> [] | n -> IOpInaccessible None :: aux (n-1) in
    Tacticals.tclTHEN (if binders <> [] then introstac (aux n) else Tacticals.tclIDTAC)
      (introstac binders) in
  let simpltac = introstac simpl in
@@ -160,7 +166,7 @@ let havetac ist
      gl, ty, Tacticals.tclTHEN assert_is_conv (Proofview.V82.of_tactic (Tactics.apply t)), id, itac_c
    | FwdHave, false, false ->
      let skols = List.flatten (List.map (function
-       | IPatAbstractVars ids -> ids
+       | IOpAbstractVars ids -> ids
        | _ -> assert false) skols) in
      let skols_args =
        List.map (fun id -> Ssripats.Internal.examine_abstract (EConstr.mkVar id) gl) skols in
@@ -203,10 +209,12 @@ let destProd_or_LetIn sigma c =
   | _ -> raise DestKO
 
 let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
+  let clr0 = Option.default [] clr0 in
+  let pats = tclCompileIPats pats in
   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 (hoi_id x) :: pats
+  | _, Some ((x, _), _) -> fun pats -> IOpId (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 +273,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, (IOpId 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 _,_ ->
@@ -289,6 +297,10 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
 (** The "suffice" tactic *)
 
 let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) =
+  let clr = Option.default [] clr in
+  let pats = tclCompileIPats pats in
+  let binders = tclCompileIPats binders in
+  let simpl = tclCompileIPats simpl in
   let htac = Tacticals.tclTHEN (introstac pats) (hinttac ist true hint) in
   let c = match Ssrcommon.ssrterm_of_ast_closure_term c with
   | (a, (b, Some ct)) ->
diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli
index 8a05e25504..35e89dbcea 100644
--- a/plugins/ssr/ssrfwd.mli
+++ b/plugins/ssr/ssrfwd.mli
@@ -22,7 +22,7 @@ val ssrposetac : Id.t * (ssrfwdfmt * ast_closure_term) -> v82tac
 
 val havetac : ist ->
            bool *
-           ((((Ssrast.ssrclear * Ssrast.ssripat list) * Ssrast.ssripats) *
+           ((((Ssrast.ssrclear option * Ssrast.ssripat list) * Ssrast.ssripats) *
              Ssrast.ssripats) *
             (((Ssrast.ssrfwdkind * 'a) * ast_closure_term) *
              (bool * Tacinterp.Value.t option list))) ->
@@ -35,7 +35,7 @@ val basecuttac :
 
 val wlogtac :
   Ltac_plugin.Tacinterp.interp_sign ->
-  ((Ssrast.ssrhyps * Ssrast.ssripats) * 'a) * 'b ->
+  ((Ssrast.ssrclear option * Ssrast.ssripats) * 'a) * 'b ->
   (Ssrast.ssrhyps *
      ((Ssrast.ssrhyp_or_id * string) *
         Ssrmatching_plugin.Ssrmatching.cpattern option)
@@ -50,7 +50,7 @@ val wlogtac :
 
 val sufftac :
   Ssrast.ist ->
-  (((Ssrast.ssrhyps * Ssrast.ssripats) * Ssrast.ssripat list) *
+  (((Ssrast.ssrclear option * Ssrast.ssripats) * Ssrast.ssripat list) *
      Ssrast.ssripat list) *
     (('a *
         ast_closure_term) *
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index ce81d83661..a8dfd69240 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -19,14 +19,78 @@ open Proofview.Notations
 
 open Ssrast
 
+type ssriop =
+  | IOpId of Names.Id.t
+  | IOpDrop
+  | IOpTemporay
+  | IOpInaccessible of string option
+  | IOpInaccessibleAll
+  | IOpAbstractVars of Names.Id.t list
+  | IOpFastNondep
+
+  | IOpInj of ssriops list
+
+  | IOpDispatchBlock of id_block
+  | IOpDispatchBranches of ssriops list
+
+  | IOpCaseBlock of id_block
+  | IOpCaseBranches of ssriops list
+
+  | IOpRewrite of ssrocc * ssrdir
+  | IOpView of ssrclear option * ssrview (* extra clears to be performed *)
+
+  | IOpClear of ssrclear * ssrhyp option (* must clear, may clear *)
+  | IOpSimpl of ssrsimpl
+
+  | IOpEqGen of unit Proofview.tactic (* generation of eqn *)
+
+  | IOpNoop
+
+and ssriops = ssriop list
+
+let rec pr_ipatop = function
+  | IOpId id -> Names.Id.print id
+  | IOpDrop -> Pp.str "_"
+  | IOpTemporay -> Pp.str "+"
+  | IOpInaccessible None -> Pp.str "?"
+  | IOpInaccessible (Some s) -> Pp.str ("?«"^s^"»")
+  | IOpInaccessibleAll -> Pp.str "*"
+  | IOpAbstractVars l -> Pp.str ("[:"^String.concat " " (List.map Names.Id.to_string l)^"]")
+  | IOpFastNondep -> Pp.str ">"
+
+  | IOpInj l -> Pp.(str "[=" ++ ppl l ++ str "]")
+
+  | IOpDispatchBlock b -> Pp.(str"(" ++ Ssrprinters.pr_block b ++ str")")
+  | IOpDispatchBranches l -> Pp.(str "(" ++ ppl l ++ str ")")
+
+  | IOpCaseBlock b -> Pp.(str"[" ++ Ssrprinters.pr_block b ++ str"]")
+  | IOpCaseBranches l -> Pp.(str "[" ++ ppl l ++ str "]")
+
+  | IOpRewrite (occ,dir) -> Pp.(Ssrprinters.(pr_occ occ ++ pr_dir dir))
+  | IOpView (None,vs) -> Pp.(prlist_with_sep mt (fun c -> str "/" ++ Ssrprinters.pr_ast_closure_term c) vs)
+  | IOpView (Some cl,vs) -> Pp.(Ssrprinters.pr_clear Pp.spc cl ++ prlist_with_sep mt (fun c -> str "/" ++ Ssrprinters.pr_ast_closure_term c) vs)
+
+  | IOpClear (clmust,clmay) ->
+      Pp.(Ssrprinters.pr_clear spc clmust ++
+            match clmay with
+            | Some cl -> str "(try " ++ Ssrprinters.pr_clear spc [cl] ++ str")"
+            | None -> mt ())
+  | IOpSimpl s -> Ssrprinters.pr_simpl s
+
+  | IOpEqGen _ -> Pp.str "E:"
+  | IOpNoop -> Pp.str"-"
+and ppl x = Pp.(prlist_with_sep (fun () -> str"|") (prlist_with_sep spc pr_ipatop)) x
+
+
 module IpatMachine : sig
 
   (* the => tactical.  ?eqtac is a tactic to be eventually run
    * after the first [..] block.  first_case_is_dispatch is the
    * ssr exception to elim: and case: *)
   val main : ?eqtac:unit tactic -> first_case_is_dispatch:bool ->
-        ssripats -> unit tactic
+        ssriops -> unit tactic
 
+  val tclCompileIPats : ssripats -> ssriops
 
   val tclSEED_SUBGOALS : Names.Name.t list array -> unit tactic -> unit tactic
 
@@ -53,7 +117,7 @@ module State : sig
   val isNSEED_CONSUME : (Names.Name.t list option -> unit tactic) -> unit tactic
 
   (* Some data may expire *)
-  val isTICK : ssripat -> unit tactic
+  val isTICK : ssriop -> unit tactic
 
   val isPRINT : Proofview.Goal.t -> Pp.t
 
@@ -149,7 +213,7 @@ let isNSEED_CONSUME k =
   k x)
 
 let isTICK = function
-  | IPatSimpl _ | IPatClear _ -> tclUNIT ()
+  | IOpSimpl _ | IOpClear _ -> tclUNIT ()
   | _ -> tclGET (fun s -> tclSET { s with name_seed = None })
 
 end (* }}} *************************************************************** *)
@@ -238,6 +302,13 @@ let tacCHECK_HYPS_EXIST hyps = Goal.enter begin fun gl ->
   tclUNIT ()
 end
 
+let tacFILTER_HYP_EXIST hyps k = Goal.enter begin fun gl ->
+  let ctx = Goal.hyps gl in
+  k (Option.bind hyps (fun h ->
+      if Ssrcommon.test_hyp_exists ctx h &&
+         Ssrcommon.(not_section_id (hyp_id h)) then Some h else None))
+end
+
 (** [=> []] *****************************************************************)
 
 (* calls t1 then t2 on each subgoal passing to t2 the index of the current
@@ -286,13 +357,13 @@ let tac_intro_seed interp_ipats fix = Goal.enter begin fun gl ->
              | Prefix id ->  Id.to_string id ^ "?"
              | SuffixNum n -> "?" ^ string_of_int n
              | SuffixId id -> "?" ^ Id.to_string id in
-           IPatAnon (One (Some s))
+           IOpInaccessible (Some s)
        | Name id ->
            let s = match fix with
              | 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 (Id.of_string s)) seeds in
+           IOpId (Id.of_string s)) seeds in
     interp_ipats ipats
 end end
 
@@ -342,7 +413,7 @@ let tclMK_ABSTRACT_VARS ids =
 (* Debugging *)
 let tclLOG p t =
   tclUNIT () >>= begin fun () ->
-    Ssrprinters.ppdebug (lazy Pp.(str "exec: " ++ Ssrprinters.pr_ipat p));
+    Ssrprinters.ppdebug (lazy Pp.(str "exec: " ++ pr_ipatop p));
     tclUNIT ()
   end <*>
   Goal.enter begin fun g ->
@@ -362,58 +433,74 @@ let tclLOG p t =
 
 let notTAC = tclUNIT false
 
+let duplicate_clear =
+  CWarnings.create ~name:"duplicate-clear" ~category:"ssr"
+    (fun id -> Pp.(str "Duplicate clear of " ++ Id.print id))
+
 (* returns true if it was a tactic (eg /ltac:tactic) *)
 let rec ipat_tac1 ipat : bool tactic =
   match ipat with
-  | IPatView (clear_if_id,l) ->
+  | IOpView (glued_clear,l) ->
+      let clear_if_id, extra_clear =
+        match glued_clear with
+        | None -> false, []
+        | Some x -> true, List.map Ssrcommon.hyp_id x in
       Ssrview.tclIPAT_VIEWS
         ~views:l ~clear_if_id
-        ~conclusion:(fun ~to_clear:clr -> intro_clear clr)
+        ~conclusion:(fun ~to_clear:clr ->
+            let inter = CList.intersect Id.equal clr extra_clear in
+            List.iter duplicate_clear inter;
+            let cl = CList.union Id.equal clr extra_clear in
+            intro_clear cl)
 
-  | IPatDispatch(true, Regular [[]]) ->
-      notTAC
-  | IPatDispatch(_, Regular ipatss) ->
+  | IOpDispatchBranches ipatss ->
       tclDISPATCH (List.map ipat_tac ipatss) <*> notTAC
-  | IPatDispatch(_,Block id_block) ->
+  | IOpDispatchBlock id_block ->
       tac_intro_seed ipat_tac id_block <*> notTAC
-
-  | IPatId id -> Ssrcommon.tclINTRO_ID id <*> notTAC
-  | IPatFastNondep -> intro_anon_deps <*> notTAC
-
-  | IPatCase (Block id_block) ->
+  | IOpCaseBlock id_block ->
       Ssrcommon.tclWITHTOP tac_case <*> tac_intro_seed ipat_tac id_block <*> notTAC
 
-  | IPatCase (Regular ipatss) ->
+  | IOpCaseBranches ipatss ->
      tclIORPAT (Ssrcommon.tclWITHTOP tac_case) ipatss <*> notTAC
-  | IPatInj ipatss ->
+
+  | IOpId id -> Ssrcommon.tclINTRO_ID id <*> notTAC
+  | IOpFastNondep -> intro_anon_deps <*> notTAC
+  | IOpDrop -> intro_drop <*> notTAC
+  | IOpInaccessible seed -> Ssrcommon.tclINTRO_ANON ?seed () <*> notTAC
+  | IOpInaccessibleAll -> intro_anon_all <*> notTAC
+  | IOpTemporay -> intro_anon_temp <*> notTAC
+
+  | IOpSimpl Nop -> assert false
+
+  | IOpInj ipatss ->
      tclIORPAT (Ssrcommon.tclWITHTOP
        (fun t -> V82.tactic  ~nf_evars:false (Ssrelim.perform_injection t)))
        ipatss
      <*> notTAC
 
-  | IPatAnon Drop -> intro_drop <*> notTAC
-  | IPatAnon (One seed) -> Ssrcommon.tclINTRO_ANON ?seed () <*> notTAC
-  | IPatAnon All -> intro_anon_all <*> notTAC
-  | IPatAnon Temporary -> intro_anon_temp <*> notTAC
-
-  | IPatNoop -> notTAC
-  | IPatSimpl Nop -> notTAC
-
-  | IPatClear ids ->
-      tacCHECK_HYPS_EXIST ids <*>
-      intro_clear (List.map Ssrcommon.hyp_id ids) <*>
+  | IOpClear (must,may) ->
+      tacCHECK_HYPS_EXIST must <*>
+      tacFILTER_HYP_EXIST may (fun may ->
+        let must = List.map Ssrcommon.hyp_id must in
+        let cl = Option.fold_left (fun cls (SsrHyp(_,id)) ->
+          if CList.mem_f Id.equal id cls then begin
+            duplicate_clear id;
+            cls
+          end else id :: cls) must may in
+        intro_clear cl) <*>
       notTAC
 
-  | IPatSimpl x ->
+  | IOpSimpl x ->
       V82.tactic ~nf_evars:false (Ssrequality.simpltac x) <*> notTAC
 
-  | IPatRewrite (occ,dir) ->
+  | IOpRewrite (occ,dir) ->
      Ssrcommon.tclWITHTOP
        (fun x -> V82.tactic  ~nf_evars:false (Ssrequality.ipat_rewrite occ dir x)) <*> notTAC
 
-  | IPatAbstractVars ids -> tclMK_ABSTRACT_VARS ids <*> notTAC
+  | IOpAbstractVars ids -> tclMK_ABSTRACT_VARS ids <*> notTAC
 
-  | IPatEqGen t -> t <*> notTAC
+  | IOpEqGen t -> t <*> notTAC
+  | IOpNoop -> notTAC
 
 and ipat_tac pl : unit tactic =
   match pl with
@@ -433,51 +520,88 @@ and tclIORPAT tac = function
   | p -> Tacticals.New.tclTHENS tac (List.map ipat_tac p)
 
 and ssr_exception is_on = function
-  | Some (IPatCase l) when is_on -> Some (IPatDispatch(true, l))
+  | Some (IOpCaseBranches [[]]) when is_on -> Some IOpNoop
+  | Some (IOpCaseBranches l) when is_on ->
+      Some (IOpDispatchBranches l)
+  | Some (IOpCaseBlock s) when is_on ->
+      Some (IOpDispatchBlock s)
   | x -> x
 
 and option_to_list = function None -> [] | Some x -> [x]
 
 and split_at_first_case ipats =
   let rec loop acc = function
-    | (IPatSimpl _ | IPatClear _) as x :: rest -> loop (x :: acc) rest
-    | (IPatCase _ | IPatDispatch _) as x :: xs -> CList.rev acc, Some x, xs
+    | (IOpSimpl _ | IOpClear _) as x :: rest -> loop (x :: acc) rest
+    | (IOpCaseBlock _ | IOpCaseBranches _
+      | IOpDispatchBlock _ | IOpDispatchBranches _) as x :: xs ->
+      CList.rev acc, Some x, xs
     | pats -> CList.rev acc, None, pats
   in
     loop [] ipats
 ;;
 
 (* Simple pass doing {x}/v ->  /v{x} *)
-let elaborate_ipats l =
+let tclCompileIPats l =
   let rec elab = function
+
+  | (IPatClear cl) :: (IPatView v) :: rest ->
+      (IOpView(Some cl,v)) :: elab rest
+  | (IPatClear cl) :: (IPatId id) :: rest ->
+      (IOpClear (cl,Some (SsrHyp(None,id)))) :: IOpId id :: elab rest
+
+  (* boring code *)
   | [] -> []
-  | (IPatClear _ as p1) :: (IPatView _ as p2) :: rest -> p2 :: p1 :: elab rest
-  | 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 _ | IPatFastNondep |
-     IPatAnon _ | IPatView _ | IPatNoop | IPatRewrite _ |
-     IPatAbstractVars _ | IPatDispatch(_, Block _) | IPatCase(Block _)) as x :: rest -> x :: elab rest
-  in
-    elab l
 
-let main ?eqtac ~first_case_is_dispatch ipats =
-  let ipats = elaborate_ipats ipats in
-  let ip_before, case, ip_after = split_at_first_case ipats in
+  | IPatId id :: rest -> IOpId id :: elab rest
+  | IPatAnon (One hint) ::rest -> IOpInaccessible hint :: elab rest
+  | IPatAnon Drop :: rest -> IOpDrop :: elab rest
+  | IPatAnon All :: rest -> IOpInaccessibleAll :: elab rest
+  | IPatAnon Temporary :: rest -> IOpTemporay :: elab rest
+  | IPatAbstractVars vs :: rest -> IOpAbstractVars vs :: elab rest
+  | IPatFastNondep :: rest -> IOpFastNondep :: elab rest
+
+  | IPatInj pats :: rest -> IOpInj (List.map elab pats) :: elab rest
+  | IPatRewrite(occ,dir) :: rest -> IOpRewrite(occ,dir) :: elab rest
+  | IPatView vs :: rest -> IOpView (None,vs) :: elab rest
+  | IPatSimpl s :: rest -> IOpSimpl s :: elab rest
+  | IPatClear cl :: rest -> IOpClear (cl,None) :: elab rest
+
+  | IPatCase (Block seed) :: rest -> IOpCaseBlock seed :: elab rest
+  | IPatCase (Regular bs) :: rest -> IOpCaseBranches (List.map elab bs) :: elab rest
+  | IPatDispatch (Block seed) :: rest -> IOpDispatchBlock seed :: elab rest
+  | IPatDispatch (Regular bs) :: rest -> IOpDispatchBranches (List.map elab bs) :: elab rest
+  | IPatNoop :: rest -> IOpNoop :: elab rest
+
+  in
+  elab l
+;;
+let tclCompileIPats l =
+  Ssrprinters.ppdebug (lazy Pp.(str "tclCompileIPats input: " ++
+                                  prlist_with_sep spc Ssrprinters.pr_ipat l));
+  let ops = tclCompileIPats l in
+  Ssrprinters.ppdebug (lazy Pp.(str "tclCompileIPats output: " ++
+                                  prlist_with_sep spc pr_ipatop ops));
+  ops
+
+let main ?eqtac ~first_case_is_dispatch iops =
+  let ip_before, case, ip_after = split_at_first_case iops in
   let case = ssr_exception first_case_is_dispatch case in
   let case = option_to_list case in
-  let eqtac = option_to_list (Option.map (fun x -> IPatEqGen x) eqtac) in
-  Ssrcommon.tcl0G ~default:() (ipat_tac (ip_before @ case @ eqtac @ ip_after) <*> intro_end)
+  let eqtac = option_to_list (Option.map (fun x -> IOpEqGen x) eqtac) in
+  let ipats = ip_before @ case @ eqtac @ ip_after in
+  Ssrcommon.tcl0G ~default:() (ipat_tac ipats <*> intro_end)
 
 end (* }}} *)
 
 let tclIPAT_EQ eqtac ip =
   Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip));
-  IpatMachine.main ~eqtac ~first_case_is_dispatch:true ip
+  IpatMachine.(main ~eqtac ~first_case_is_dispatch:true (tclCompileIPats ip))
 
 let tclIPATssr ip =
   Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip));
-  IpatMachine.main ~first_case_is_dispatch:true ip
+  IpatMachine.(main ~first_case_is_dispatch:true (tclCompileIPats ip))
+
+let tclCompileIPats = IpatMachine.tclCompileIPats
 
 (* Common code to handle generalization lists along with the defective case *)
 let with_defective maintac deps clr = Goal.enter begin fun g ->
@@ -721,12 +845,12 @@ let eqmovetac _ gen =
 ;;
 
 let rec eqmoveipats eqpat = function
-  | (IPatSimpl _ | IPatClear _ as ipat) :: ipats ->
+  | (IOpSimpl _ | IOpClear _ as ipat) :: ipats ->
        ipat :: eqmoveipats eqpat ipats
-  | (IPatAnon All :: _ | []) as ipats ->
-       IPatAnon (One None) :: eqpat :: ipats
+  | (IOpInaccessibleAll :: _ | []) as ipats ->
+       IOpInaccessible None :: eqpat @ ipats
   | ipat :: ipats ->
-       ipat :: eqpat :: ipats
+       ipat :: eqpat @ ipats
 
 let ssrsmovetac = Goal.enter begin fun g ->
   let sigma, concl = Goal.(sigma g, concl g) in
@@ -736,7 +860,6 @@ let ssrsmovetac = Goal.enter begin fun g ->
 end
 
 let tclIPAT ip =
-  Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip));
   IpatMachine.main ~first_case_is_dispatch:false ip
 
 let ssrmovetac = function
@@ -748,17 +871,17 @@ let ssrmovetac = function
      gentac <*>
      tclLAST_GEN ~to_ind:false lastgen
        (tacVIEW_THEN_GRAB view ~conclusion) <*>
-     tclIPAT (IPatClear clr :: ipats)
+     tclIPAT (IOpClear (clr,None) :: IpatMachine.tclCompileIPats ipats)
   | _::_ as view, (_, ({ gens = []; clr }, ipats)) ->
-     tclIPAT (IPatView (false,view) :: IPatClear clr :: ipats)
+      tclIPAT (IOpView (None,view) :: IOpClear (clr,None) :: IpatMachine.tclCompileIPats ipats)
   | _, (Some pat, (dgens, ipats)) ->
     let dgentac = with_dgens dgens eqmovetac in
-    dgentac <*> tclIPAT (eqmoveipats pat ipats)
+    dgentac <*> tclIPAT (eqmoveipats (IpatMachine.tclCompileIPats [pat]) (IpatMachine.tclCompileIPats ipats))
   | _, (_, ({ gens = (_ :: _ as gens); dgens = []; clr}, ipats)) ->
     let gentac = V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, clr)) in
-    gentac <*> tclIPAT ipats
+    gentac <*> tclIPAT (IpatMachine.tclCompileIPats ipats)
   | _, (_, ({ clr }, ipats)) ->
-    Tacticals.New.tclTHENLIST [ssrsmovetac; Tactics.clear (List.map Ssrcommon.hyp_id clr); tclIPAT ipats]
+    Tacticals.New.tclTHENLIST [ssrsmovetac; Tactics.clear (List.map Ssrcommon.hyp_id clr); tclIPAT (IpatMachine.tclCompileIPats ipats)]
 
 (** [abstract: absvar gens] **************************************************)
 let rec is_Evar_or_CastedMeta sigma x =
diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli
index 89cba4be71..893061b154 100644
--- a/plugins/ssr/ssripats.mli
+++ b/plugins/ssr/ssripats.mli
@@ -19,8 +19,44 @@
 
 open Ssrast
 
+(* Atomic operations for the IPat machine. Use this if you are "patching" an
+ * ipat written by the user, since patching it at he AST level and then
+ * compiling it may have tricky effects, eg adding a clear in front of a view
+ * also has the effect of disposing the view (the compilation phase takes care
+ * of this, by using the compiled ipats you can be more precise *)
+type ssriop =
+  | IOpId of Names.Id.t
+  | IOpDrop
+  | IOpTemporay
+  | IOpInaccessible of string option
+  | IOpInaccessibleAll
+  | IOpAbstractVars of Names.Id.t list
+  | IOpFastNondep
+
+  | IOpInj of ssriops list
+
+  | IOpDispatchBlock of id_block
+  | IOpDispatchBranches of ssriops list
+
+  | IOpCaseBlock of id_block
+  | IOpCaseBranches of ssriops list
+
+  | IOpRewrite of ssrocc * ssrdir
+  | IOpView of ssrclear option * ssrview (* extra clears to be performed *)
+
+  | IOpClear of ssrclear * ssrhyp option
+  | IOpSimpl of ssrsimpl
+
+  | IOpEqGen of unit Proofview.tactic (* generation of eqn *)
+
+  | IOpNoop
+
+and ssriops = ssriop list
+
+val tclCompileIPats : ssripats -> ssriops
+
 (* The => tactical *)
-val tclIPAT : ssripats -> unit Proofview.tactic
+val tclIPAT : ssriops -> unit Proofview.tactic
 
 (* As above but with the SSR exception: first case is dispatch *)
 val tclIPATssr : ssripats -> unit Proofview.tactic
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 76726009ac..3fb21e5ef6 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -635,11 +635,10 @@ let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function
   | 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))
   | IPatCase (Block(hat)) -> IPatCase (Block(map_block map_id hat))
-  | IPatDispatch (s, Regular iorpat) -> IPatDispatch (s, Regular (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat))
-  | IPatDispatch (s, Block (hat)) -> IPatDispatch (s, Block(map_block map_id hat))
+  | IPatDispatch (Regular iorpat) -> IPatDispatch (Regular (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat))
+  | IPatDispatch (Block (hat)) -> IPatDispatch (Block(map_block map_id hat))
   | IPatInj iorpat -> IPatInj (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)
-  | IPatView (clr,v) -> IPatView (clr,List.map map_ast_closure_term v)
-  | IPatEqGen _ -> assert false (*internal usage only *)
+  | IPatView v -> IPatView (List.map map_ast_closure_term v)
 and map_block map_id = function
   | Prefix id -> Prefix (map_id id)
   | SuffixId id -> SuffixId (map_id id)
@@ -715,22 +714,22 @@ let interp_ipat ist gl =
       if not (ltacvar id) then hyp :: hyps else
       add_intro_pattern_hyps CAst.(make ?loc (interp_introid ist gl id)) hyps in
     let clr' = List.fold_right add_hyps clr [] in
-    check_hyps_uniq [] clr'; IPatClear clr'
+    check_hyps_uniq [] clr';
+    IPatClear clr'
   | IPatCase(Regular iorpat) ->
       IPatCase(Regular(List.map (List.map interp) iorpat))
   | IPatCase(Block(hat)) -> IPatCase(Block(interp_block hat))
 
-  | IPatDispatch(s,Regular iorpat) ->
-      IPatDispatch(s,Regular (List.map (List.map interp) iorpat))
-  | IPatDispatch(s,Block(hat)) -> IPatDispatch(s,Block(interp_block hat))
+  | IPatDispatch(Regular iorpat) ->
+      IPatDispatch(Regular (List.map (List.map interp) iorpat))
+  | IPatDispatch(Block(hat)) -> IPatDispatch(Block(interp_block hat))
 
   | IPatInj iorpat -> IPatInj (List.map (List.map interp) iorpat)
   | IPatAbstractVars l ->
      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
+  | IPatView l -> IPatView (List.map (fun x -> snd(interp_ast_closure_term ist
      gl x)) l)
   | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop | IPatFastNondep) as x -> x
-  | IPatEqGen _ -> assert false (*internal usage only *)
     in
   interp
 
@@ -765,10 +764,6 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY { pr_ssripats }
       | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected")
       | None, occ ->  [IPatRewrite (occ, R2L)]
       | Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, R2L)] }
-  | [ ssrdocc(occ) ssrfwdview(v) ] -> { match occ with
-      | Some [], _ -> [IPatView (true,v)]
-      | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl;IPatView (false,v)]
-      | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here") }
   | [ ssrdocc(occ) ] -> { match occ with
       | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl]
       | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here") }
@@ -786,7 +781,7 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY { pr_ssripats }
   | [ "-/" integer(n) "/=" ] -> { [IPatNoop;IPatSimpl(SimplCut (n,~-1))] }
   | [ "-/" integer(n) "/" integer (m) "=" ] ->
       { [IPatNoop;IPatSimpl(SimplCut(n,m))] }
-  | [ ssrfwdview(v) ] -> { [IPatView (false,v)] }
+  | [ ssrfwdview(v) ] -> { [IPatView v] }
   | [ "[" ":" ident_list(idl) "]" ] -> { [IPatAbstractVars idl] }
   | [ "[:" ident_list(idl) "]" ] -> { [IPatAbstractVars idl] }
 END
@@ -875,11 +870,12 @@ ARGUMENT EXTEND ssripats_ne TYPED AS ssripat PRINTED BY { pr_ssripats }
 let check_ssrhpats loc w_binders ipats =
   let err_loc s = CErrors.user_err ~loc ~hdr:"ssreflect" s in
   let clr, ipats =
+    let opt_app = function None -> fun l -> Some l
+      | Some l1 -> fun l2 -> Some (l1 @ l2) in 
     let rec aux clr = function
-      | IPatClear cl :: tl -> aux (clr @ cl) tl
-(*      | IPatSimpl (cl, sim) :: tl -> clr @ cl, IPatSimpl ([], sim) :: tl *)
+      | IPatClear cl :: tl -> aux (opt_app clr cl) tl
       | tl -> clr, tl
-    in aux [] ipats in
+    in aux None ipats in
   let simpl, ipats = 
     match List.rev ipats with
     | IPatSimpl _ as s :: tl -> [s], List.rev tl
@@ -903,27 +899,29 @@ let check_ssrhpats loc w_binders ipats =
     in loop [] ipats in
   ((clr, ipat), binders), simpl
 
+let pr_clear_opt sep = function None -> mt () | Some x -> pr_clear sep x
+
 let pr_hpats (((clr, ipat), binders), simpl) =
-   pr_clear mt clr ++ pr_ipats ipat ++ pr_ipats binders ++ pr_ipats simpl
+   pr_clear_opt mt clr ++ pr_ipats ipat ++ pr_ipats binders ++ pr_ipats simpl
 let pr_ssrhpats _ _ _ = pr_hpats
 let pr_ssrhpats_wtransp _ _ _ (_, x) = pr_hpats x
 
 }
 
-ARGUMENT EXTEND ssrhpats TYPED AS (((ssrclear * ssripat) * ssripat) * ssripat)
+ARGUMENT EXTEND ssrhpats TYPED AS (((ssrclear option * ssripat) * ssripat) * ssripat)
 PRINTED BY { pr_ssrhpats }
   | [ ssripats(i) ] -> { check_ssrhpats loc true i }
 END
 
 ARGUMENT EXTEND ssrhpats_wtransp
-  TYPED AS (bool * (((ssrclear * ssripats) * ssripats) * ssripats))
+  TYPED AS (bool * (((ssrclear option * ssripats) * ssripats) * ssripats))
   PRINTED BY { pr_ssrhpats_wtransp }
   | [ ssripats(i) ] -> { false,check_ssrhpats loc true i }
   | [ ssripats(i) "@" ssripats(j) ] -> { true,check_ssrhpats loc true (i @ j) }
 END
 
 ARGUMENT EXTEND ssrhpats_nobs 
-TYPED AS (((ssrclear * ssripats) * ssripats) * ssripats) PRINTED BY { pr_ssrhpats }
+TYPED AS (((ssrclear option * ssripats) * ssripats) * ssripats) PRINTED BY { pr_ssrhpats }
   | [ ssripats(i) ] -> { check_ssrhpats loc false i }
 END
 
@@ -2051,7 +2049,7 @@ END
 (* We just add a numeric version that clears the n top assumptions. *)
 
 TACTIC EXTEND ssrclear
-  | [ "clear" natural(n) ] -> { tclIPAT (List.init n (fun _ -> IPatAnon Drop)) }
+  | [ "clear" natural(n) ] -> { tclIPAT (List.init n (fun _ -> IOpDrop)) }
 END
 
 (** The "move" tactic *)
@@ -2090,10 +2088,10 @@ let movearg_of_parsed_movearg (v,(eq,(dg,ip))) =
 
 TACTIC EXTEND ssrmove
 | [ "move" ssrmovearg(arg) ssrrpat(pat) ] ->
-  { ssrmovetac (movearg_of_parsed_movearg arg) <*> tclIPAT [pat] }
+  { ssrmovetac (movearg_of_parsed_movearg arg) <*> tclIPAT (tclCompileIPats [pat]) }
 | [ "move" ssrmovearg(arg) ssrclauses(clauses) ] ->
   { tclCLAUSES (ssrmovetac (movearg_of_parsed_movearg arg)) clauses }
-| [ "move" ssrrpat(pat) ] -> { tclIPAT [pat] }
+| [ "move" ssrrpat(pat) ] -> { tclIPAT (tclCompileIPats [pat]) }
 | [ "move" ] -> { ssrsmovetac }
 END
 
@@ -2632,7 +2630,11 @@ END
 
 {
 
-let augment_preclr clr1 (((clr0, x),y),z) = (((clr1 @ clr0, x),y),z)
+let augment_preclr clr1 (((clr0, x),y),z) =
+  let cl = match clr0 with
+    | None -> if clr1 = [] then None else Some clr1
+    | Some clr0 -> Some (clr1 @ clr0) in
+  (((cl, x),y),z)
 
 }
 
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index 898e03b00e..38f5b7d107 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -74,7 +74,7 @@ let pr_occ = function
   | None -> str "{}"
 
 let pr_clear_ne clr = str "{" ++ pr_hyps clr ++ str "}"
-let pr_clear sep clr = if clr = [] then mt () else sep () ++ pr_clear_ne clr
+let pr_clear sep clr = sep () ++ pr_clear_ne clr
 
 let pr_dir = function L2R -> str "->" | R2L -> str "<-"
 
@@ -102,20 +102,18 @@ let rec pr_ipat p =
   | IPatClear clr -> pr_clear mt clr
   | 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")")
+  | 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 "?"
-  | IPatView (false,v) -> pr_view2 v
-  | IPatView (true,v) -> str"{}" ++ pr_view2 v
+  | IPatView v -> pr_view2 v
   | 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
 and pr_block = function (Prefix id) -> str"^" ++ Id.print id
diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli
index 31c360ad6d..5f20ac2705 100644
--- a/plugins/ssr/ssrprinters.mli
+++ b/plugins/ssr/ssrprinters.mli
@@ -43,6 +43,7 @@ val pr_view2 : ast_closure_term list -> Pp.t
 val pr_ipat : ssripat -> Pp.t
 val pr_ipats : ssripats -> Pp.t
 val pr_iorpat : ssripatss -> Pp.t
+val pr_block : id_block -> Pp.t
 
 val pr_hyp : ssrhyp -> Pp.t
 val pr_hyps : ssrhyps -> Pp.t
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 4816027296..2794696017 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -142,7 +142,7 @@ let intern_constr_expr { Genintern.genv; ltacvars = vars } sigma ce =
    To allow for t being a notation, like "Notation foo x := ltac:(foo x)", we
    need to internalize t.
 *)
-let is_tac_in_term ?extra_scope { body; glob_env; interp_env } =
+let is_tac_in_term ?extra_scope { annotation; body; glob_env; interp_env } =
   Goal.(enter_one ~__LOC__ begin fun goal ->
     let genv = env goal in
     let sigma = sigma goal in
@@ -161,7 +161,7 @@ let is_tac_in_term ?extra_scope { body; glob_env; interp_env } =
     | Glob_term.GHole (_,_, Some x)
       when Genarg.has_type x (Genarg.glbwit Tacarg.wit_tactic)
         -> tclUNIT (`Tac (Genarg.out_gen (Genarg.glbwit Tacarg.wit_tactic) x))
-    | _ -> tclUNIT (`Term (interp_env, g))
+    | _ -> tclUNIT (`Term (annotation, interp_env, g))
 end)
 
 (* To inject a constr into a glob_constr we use an Ltac variable *)
@@ -207,7 +207,7 @@ let tclKeepOpenConstr (_env, sigma, t) = Unsafe.tclEVARS sigma <*> tclUNIT t
 let tclADD_CLEAR_IF_ID (env, ist, t) x =
   Ssrprinters.ppdebug (lazy
     Pp.(str"tclADD_CLEAR_IF_ID: " ++ Printer.pr_econstr_env env ist t));
-  let hd, _ = EConstr.decompose_app ist t in
+  let hd, args = EConstr.decompose_app ist t in
   match EConstr.kind ist hd with
   | Constr.Var id when Ssrcommon.not_section_id id -> tclUNIT (x, [id])
   | _ -> tclUNIT (x,[])
@@ -280,8 +280,9 @@ let interp_view ~clear_if_id ist v p =
        else tclKeepOpenConstr ot >>= tclPAIR []
 
 (* we store in the state (v top), then (v1 (v2 top))... *)
-let pile_up_view ~clear_if_id (ist, v) =
+let pile_up_view ~clear_if_id (annotation, ist, v) =
   let ist = Ssrcommon.option_assert_get ist (Pp.str"not a term") in
+  let clear_if_id = clear_if_id && annotation <> `Parens in
   State.vsPUSH (fun p -> interp_view ~clear_if_id ist v p)
 
 let finalize_view s0 ?(simple_types=true) p =