Merge PR #7236: [ssr] simpler semantics for delayed clears

9 files changed, 166 insertions, 65 deletions

diff --git a/CHANGES b/CHANGES
index c36f59726..6ad2cc548 100644
--- a/CHANGES
+++ b/CHANGES
@@ -61,6 +61,26 @@ Coq binaries and process model
   `coq{proof,tactic,query}worker` are in charge of task-specific and
   parallel proof checking.
 
+SSReflect
+
+- The implementation of delayed clear switches in intro patterns
+  is now simpler to explain:
+  1. The immediate effect of a clear switch like {x} is to rename the
+     variable x to _x_ (i.e. a reserved identifier that cannot be mentioned
+     explicitly)
+  2. The delayed effect of {x} is that _x_ is cleared at the end of the intro
+     pattern
+  3. A clear switch immediately before a view application like {x}/v is
+     translated to /v{x}.
+  In particular rule 3 lets one write {x}/v even if v uses the variable x:
+  indeed the view is executed before the renaming.
+
+- An empty clear switch is now accepted in intro patterns before a 
+  view application whenever the view is a variable.
+  One can now write {}/v to mean {v}/v.  Remark that {}/x is very similar
+  to the idiom {}e for the rewrite tactic (the equation e is used for
+  rewriting and then discarded).
+
 Changes from 8.8.0 to 8.8.1
 ===========================
 
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index ab52c2ce7..6fb73a030 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -623,7 +623,9 @@ where:
 + In the occurrence switch :token:`occ_switch`, if the first element of the
   list is a natural, this element should be a number, and not an Ltac
   variable. The empty list ``{}`` is not interpreted as a valid occurrence
-  switch.
+  switch, it is rather used as a flag to signal the intent of the user to
+  clear the name following it (see :ref:`ssr_rewrite_occ_switch` and
+  :ref:`introduction_ssr`)
 
 The tactic:
 
@@ -1539,7 +1541,7 @@ whose general syntax is
    :name: =>
 
 .. prodn::
-   i_item ::= @i_pattern %| @s_item %| @clear_switch %| /@term
+   i_item ::= @i_pattern %| @s_item %| @clear_switch %| {? %{%} } /@term
 
 .. prodn::
    s_item ::= /= %| // %| //=
@@ -1641,6 +1643,11 @@ The view is applied to the top assumption.
   While it is good style to use the :token:`i_item` i * to pop the variables
   and assumptions corresponding to each constructor, this is not enforced by
   |SSR|.
+``/`` :token:`term`
+  Interprets the top of the stack with the view :token:`term`.
+  It is equivalent to ``move/term``. The optional flag ``{}`` can
+  be used to signal that the :token:`term`, when it is a context entry,
+  has to be cleared.
 ``-``
   does nothing, but counts as an intro pattern. It can also be used to
   force the interpretation of ``[`` :token:`i_item` * ``| … |``
@@ -3236,6 +3243,7 @@ the equality.
   Indeed the left hand side of ``H`` does not match
   the redex identified by the pattern ``x + y * 4``.
 
+.. _ssr_rewrite_occ_switch:
 
 Occurrence switches and redex switches
 ``````````````````````````````````````
@@ -3260,6 +3268,9 @@ the rewrite tactic. The effect of the tactic on the initial goal is to
 rewrite this lemma at the second occurrence of the first matching
 ``x + y + 0`` of the explicit rewrite redex ``_ + y + 0``.
 
+An empty occurrence switch ``{}`` is not interpreted as a valid occurrence
+switch. It has the effect of clearing the :token:`r_item` (when it is the name
+of a context entry).
 
 Occurrence selection and repetition
 ```````````````````````````````````
@@ -5279,7 +5290,7 @@ generalization item see :ref:`structure_ssr`
 
 intro pattern :ref:`introduction_ssr`
 
-.. prodn:: i_item ::= @clear_switch %| @s_item %| @i_pattern %| / @term
+.. prodn:: i_item ::= @clear_switch %| @s_item %| @i_pattern %| {? %{%} } / @term
 
 intro item  see :ref:`introduction_ssr`
 
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index 5571c5420..6ba937a2f 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -88,7 +88,7 @@ type ssripat =
   | IPatCase of (* ipats_mod option * *) ssripatss (* this is not equivalent to /case /[..|..] if there are already multiple goals *)
   | IPatInj of ssripatss
   | IPatRewrite of (*occurrence option * rewrite_pattern **) ssrocc * ssrdir
-  | IPatView of ssrview (* /view *)
+  | IPatView of bool * ssrview (* {}/view (true if the clear is present) *)
   | IPatClear of ssrclear (* {H1 H2} *)
   | IPatSimpl of ssrsimpl
   | IPatAbstractVars of Id.t list
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 8207bc11e..46fde4115 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -119,13 +119,10 @@ let intro_end =
   Ssrcommon.tcl0G (isCLR_CONSUME)
 
 (** [=> _] *****************************************************************)
-let intro_clear ids future_ipats =
+let intro_clear ids =
   Goal.enter begin fun gl ->
     let _, clear_ids, ren =
       List.fold_left (fun (used_ids, clear_ids, ren) id ->
-          if not(Ssrcommon.is_name_in_ipats id future_ipats) then begin
-            used_ids, id :: clear_ids, ren
-          end else
             let new_id = Ssrcommon.mk_anon_id (Id.to_string id) used_ids in
             (new_id :: used_ids, new_id :: clear_ids, (id, new_id) :: ren))
                      (Tacmach.New.pf_ids_of_hyps gl, [], []) ids
@@ -213,22 +210,22 @@ let tclLOG p t =
     tclUNIT ()
   end
 
-let rec ipat_tac1 future_ipats ipat : unit tactic =
+let rec ipat_tac1 ipat : unit tactic =
   match ipat with
-  | IPatView l ->
-      Ssrview.tclIPAT_VIEWS ~views:l
-        ~conclusion:(fun ~to_clear:clr -> intro_clear clr future_ipats)
+  | IPatView (clear_if_id,l) ->
+      Ssrview.tclIPAT_VIEWS ~views:l ~clear_if_id
+        ~conclusion:(fun ~to_clear:clr -> intro_clear clr)
   | IPatDispatch ipatss ->
-      tclEXTEND (List.map (ipat_tac future_ipats) ipatss) (tclUNIT ()) []
+      tclEXTEND (List.map ipat_tac ipatss) (tclUNIT ()) []
 
   | IPatId id -> Ssrcommon.tclINTRO_ID id
 
   | IPatCase ipatss ->
-     tclIORPAT (Ssrcommon.tclWITHTOP tac_case) future_ipats ipatss
+     tclIORPAT (Ssrcommon.tclWITHTOP tac_case) ipatss
   | IPatInj ipatss ->
      tclIORPAT (Ssrcommon.tclWITHTOP
        (fun t -> V82.tactic  ~nf_evars:false (Ssrelim.perform_injection t)))
-       future_ipats ipatss
+       ipatss
 
   | IPatAnon Drop -> intro_drop
   | IPatAnon One -> Ssrcommon.tclINTRO_ANON
@@ -239,7 +236,7 @@ let rec ipat_tac1 future_ipats ipat : unit tactic =
 
   | IPatClear ids ->
       tacCHECK_HYPS_EXIST ids <*>
-      intro_clear (List.map Ssrcommon.hyp_id ids) future_ipats
+      intro_clear (List.map Ssrcommon.hyp_id ids)
 
   | IPatSimpl (Simpl n) ->
        V82.tactic ~nf_evars:false (Ssrequality.simpltac (Simpl n))
@@ -256,17 +253,17 @@ let rec ipat_tac1 future_ipats ipat : unit tactic =
 
   | IPatTac t -> t
 
-and ipat_tac future_ipats pl : unit tactic =
+and ipat_tac pl : unit tactic =
   match pl with
   | [] -> tclUNIT ()
   | pat :: pl ->
-      Ssrcommon.tcl0G (tclLOG pat (ipat_tac1 (pl @ future_ipats))) <*>
+      Ssrcommon.tcl0G (tclLOG pat ipat_tac1) <*>
       isTICK pat <*>
-      ipat_tac future_ipats pl
+      ipat_tac pl
 
-and tclIORPAT tac future_ipats = function
+and tclIORPAT tac = function
   | [[]] -> tac
-  | p -> Tacticals.New.tclTHENS tac (List.map (ipat_tac future_ipats) p)
+  | p -> Tacticals.New.tclTHENS tac (List.map ipat_tac p)
 
 let split_at_first_case ipats =
   let rec loop acc = function
@@ -282,12 +279,27 @@ let ssr_exception is_on = function
 
 let option_to_list = function None -> [] | Some x -> [x]
 
+(* Simple pass doing {x}/v ->  /v{x} *)
+let elaborate_ipats l =
+  let rec elab = function
+  | [] -> []
+  | (IPatClear _ as p1) :: (IPatView _ as p2) :: rest -> p2 :: p1 :: elab rest
+  | IPatDispatch p :: rest -> IPatDispatch (List.map elab p) :: elab rest
+  | IPatCase p :: rest -> IPatCase (List.map elab p) :: elab rest
+  | IPatInj p :: rest -> IPatInj (List.map elab p) :: elab rest
+  | (IPatTac _ | IPatId _ | IPatSimpl _ | IPatClear _ |
+     IPatAnon _ | IPatView _ | IPatNoop | IPatRewrite _ |
+     IPatAbstractVars _) 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
   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 -> IPatTac x) eqtac) in
-  Ssrcommon.tcl0G (ipat_tac [] (ip_before @ case @ eqtac @ ip_after) <*> intro_end)
+  Ssrcommon.tcl0G (ipat_tac (ip_before @ case @ eqtac @ ip_after) <*> intro_end)
 
 end (* }}} *)
 
@@ -576,7 +588,7 @@ let ssrmovetac = function
        (tacVIEW_THEN_GRAB view ~conclusion) <*>
      tclIPAT (IPatClear clr :: ipats)
   | _::_ as view, (_, ({ gens = []; clr }, ipats)) ->
-     tclIPAT (IPatView view :: IPatClear clr :: ipats)
+     tclIPAT (IPatView (false,view) :: IPatClear clr :: ipats)
   | _, (Some pat, (dgens, ipats)) ->
     let dgentac = with_dgens dgens eqmovetac in
     dgentac <*> tclIPAT (eqmoveipats pat ipats)
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 7a1d06fdc..347a1e4e2 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -412,8 +412,8 @@ let pr_docc = function
 let pr_ssrdocc _ _ _ = pr_docc
 
 ARGUMENT EXTEND ssrdocc TYPED AS ssrclear option * ssrocc PRINTED BY pr_ssrdocc
-| [ "{" ne_ssrhyp_list(clr) "}" ] -> [ mkclr clr ]
 | [ "{" ssrocc(occ) "}" ] -> [ mkocc occ ]
+| [ "{" ssrhyp_list(clr) "}" ] -> [ mkclr clr ]
 END
 
 (* Old kinds of terms *)
@@ -578,7 +578,7 @@ let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function
   | IPatCase iorpat -> IPatCase (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)
   | IPatDispatch iorpat -> IPatDispatch (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)
   | IPatInj iorpat -> IPatInj (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)
-  | IPatView v -> IPatView (List.map map_ast_closure_term v)
+  | IPatView (clr,v) -> IPatView (clr,List.map map_ast_closure_term v)
   | IPatTac _ -> assert false (*internal usage only *)
 
 let wit_ssripatrep = add_genarg "ssripatrep" pr_ipat
@@ -646,7 +646,7 @@ let interp_ipat ist gl =
   | 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 l -> IPatView (List.map (fun x -> snd(interp_ast_closure_term ist
+  | 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
   | IPatTac _ -> assert false (*internal usage only *)
@@ -683,11 +683,17 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY pr_ssripats
 (* TODO  | [ "+" ] -> [ [IPatAnon Temporary] ] *)
   | [ ssrsimpl_ne(sim) ] -> [ [IPatSimpl sim] ]
   | [ ssrdocc(occ) "->" ] -> [ match occ with
+      | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected")
       | None, occ -> [IPatRewrite (occ, L2R)]
       | Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, L2R)]]
   | [ ssrdocc(occ) "<-" ] -> [ match occ with
+      | 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")]
@@ -705,7 +711,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 v] ]
+  | [ ssrfwdview(v) ] -> [ [IPatView (false,v)] ]
   | [ "[" ":" ident_list(idl) "]" ] -> [ [IPatAbstractVars idl] ]
   | [ "[:" ident_list(idl) "]" ] -> [ [IPatAbstractVars idl] ]
 END
@@ -1678,7 +1684,10 @@ let pr_gen (docc, dt) = pr_docc docc ++ pr_cpattern dt
 let pr_ssrgen _ _ _ = pr_gen
 
 ARGUMENT EXTEND ssrgen TYPED AS ssrdocc * cpattern PRINTED BY pr_ssrgen
-| [ ssrdocc(docc) cpattern(dt) ] -> [ docc, dt ]
+| [ ssrdocc(docc) cpattern(dt) ] -> [
+     match docc with
+     | Some [], _ -> CErrors.user_err ~loc (str"Clear flag {} not allowed here")
+     | _ -> docc, dt ]
 | [ cpattern(dt) ] -> [ nodocc, dt ]
 END
 
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index 11369228c..8f4b2179e 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -107,7 +107,8 @@ let rec pr_ipat p =
   | IPatAnon All -> str "*"
   | IPatAnon Drop -> str "_"
   | IPatAnon One -> str "?"
-  | IPatView v -> pr_view2 v
+  | IPatView (false,v) -> pr_view2 v
+  | IPatView (true,v) -> str"{}" ++ pr_view2 v
   | IPatNoop -> str "-"
   | IPatAbstractVars l -> str "[:" ++ pr_list spc Id.print l ++ str "]"
   | IPatTac _ -> str "<tac>"
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index faebe3179..3f974ea06 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -67,9 +67,9 @@ end
 module State : sig
 
   (* View storage API *)
-  val vsINIT    : EConstr.t -> unit tactic
-  val vsPUSH    : (EConstr.t -> EConstr.t tactic) -> unit tactic
-  val vsCONSUME : (Id.t option -> EConstr.t -> unit tactic) -> unit tactic
+  val vsINIT    : EConstr.t * Id.t list -> unit tactic
+  val vsPUSH    : (EConstr.t -> (EConstr.t * Id.t list) tactic) -> unit tactic
+  val vsCONSUME : (name:Id.t option -> EConstr.t -> to_clear:Id.t list -> unit tactic) -> unit tactic
   val vsASSERT_EMPTY : unit tactic
 
 end = struct (* {{{ *)
@@ -78,6 +78,7 @@ type vstate = {
   subject_name : Id.t option;   (* top *)
     (* None if views are being applied to a term *)
   view : EConstr.t;  (* v2 (v1 top) *)
+  to_clear : Id.t list;
 }
 
 include Ssrcommon.MakeState(struct
@@ -85,13 +86,14 @@ include Ssrcommon.MakeState(struct
   let init = None
 end)
 
-let vsINIT view = tclSET (Some { subject_name = None; view })
+let vsINIT (view, to_clear) =
+  tclSET (Some { subject_name = None; view; to_clear })
 
 let vsPUSH k =
   tacUPDATE (fun s -> match s with
-  | Some { subject_name; view } ->
-      k view >>= fun view ->
-      tclUNIT (Some { subject_name; view })
+  | Some { subject_name; view; to_clear } ->
+      k view >>= fun (view, clr) ->
+      tclUNIT (Some { subject_name; view; to_clear = to_clear @ clr })
   | None ->
       Goal.enter_one ~__LOC__ begin fun gl ->
         let concl = Goal.concl gl in
@@ -102,15 +104,15 @@ let vsPUSH k =
           | _ -> mk_anon_id "view_subject" (Tacmach.New.pf_ids_of_hyps gl) in
         let view = EConstr.mkVar id in
         Ssrcommon.tclINTRO_ID id <*>
-        k view >>= fun view ->
-        tclUNIT (Some { subject_name = Some id; view })
+        k view >>= fun (view, to_clear) ->
+        tclUNIT (Some { subject_name = Some id; view; to_clear })
       end)
 
 let vsCONSUME k =
   tclGET (fun s -> match s with
-  | Some { subject_name; view } ->
+  | Some { subject_name; view; to_clear } ->
         tclSET None <*>
-        k subject_name view
+        k ~name:subject_name view ~to_clear
   | None -> anomaly "vsCONSUME: empty storage")
 
 let vsASSERT_EMPTY =
@@ -187,6 +189,16 @@ end
  * modular, see the 2 functions below that would need to "uncommit" *)
 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
+  match EConstr.kind ist hd with
+  | Constr.Var id when Ssrcommon.not_section_id id -> tclUNIT (x, [id])
+  | _ -> tclUNIT (x,[])
+
+let tclPAIR p x = tclUNIT (x, p)
+
 (* The ssr heuristic : *)
 (* Estimate a bound on the number of arguments of a raw constr. *)
 (* This is not perfect, because the unifier may fail to         *)
@@ -203,14 +215,15 @@ let guess_max_implicits ist glob =
   (fun _ -> tclUNIT 5)
 
 let pad_to_inductive ist glob = Goal.enter_one ~__LOC__ begin fun goal ->
-  interp_glob ist glob >>= fun (env, sigma, term) ->
+  interp_glob ist glob >>= fun (env, sigma, term as ot) ->
   let term_ty = Retyping.get_type_of env sigma term in
   let ctx, i = Reductionops.splay_prod env sigma term_ty in
   let rel_ctx =
     List.map (fun (a,b) -> Context.Rel.Declaration.LocalAssum(a,b)) ctx in
-  if Ssrcommon.isAppInd (EConstr.push_rel_context rel_ctx env) sigma i
-  then tclUNIT (mkGApp glob (mkGHoles (List.length ctx)))
-  else Tacticals.New.tclZEROMSG Pp.(str"not an inductive")
+  if not (Ssrcommon.isAppInd (EConstr.push_rel_context rel_ctx env) sigma i)
+  then Tacticals.New.tclZEROMSG Pp.(str"not an inductive")
+  else tclUNIT (mkGApp glob (mkGHoles (List.length ctx)))
+       >>= tclADD_CLEAR_IF_ID ot
 end
 
 (* There are two ways of "applying" a view to term:            *)
@@ -221,7 +234,7 @@ end
 (* They require guessing the view hints and the number of      *)
 (* implicits, respectively, which we do by brute force.        *)
 (* Builds v p *)
-let interp_view ist v p =
+let interp_view ~clear_if_id ist v p =
   let is_specialize hd =
     match DAst.get hd with Glob_term.GHole _ -> true | _ -> false in
   (* We cast the pile of views p into a term p_id *)
@@ -230,25 +243,31 @@ let interp_view ist v p =
   match DAst.get v with
   | Glob_term.GApp (hd, rargs) when is_specialize hd ->
      Ssrprinters.ppdebug (lazy Pp.(str "specialize"));
-     interp_glob ist (mkGApp p_id rargs) >>= tclKeepOpenConstr
+     interp_glob ist (mkGApp p_id rargs)
+     >>= tclKeepOpenConstr >>= tclPAIR []
   | _ ->
      Ssrprinters.ppdebug (lazy Pp.(str "view"));
      (* We find out how to build (v p) eventually using an adaptor *)
      let adaptors = AdaptorDb.(get Forward) in
      Proofview.tclORELSE
-       (pad_to_inductive ist v >>= fun vpad ->
+       (pad_to_inductive ist v >>= fun (vpad,clr) ->
         Ssrcommon.tclFIRSTa (List.map
-          (fun a -> interp_glob ist (mkGApp a [vpad; p_id])) adaptors))
+          (fun a -> interp_glob ist (mkGApp a [vpad; p_id])) adaptors)
+        >>= tclPAIR clr)
        (fun _ ->
         guess_max_implicits ist v >>= fun n ->
         Ssrcommon.tclFIRSTi (fun n ->
-           interp_glob ist (mkGApp v (mkGHoles n @ [p_id]))) n)
-     >>= tclKeepOpenConstr
+           interp_glob ist (mkGApp v (mkGHoles n @ [p_id]))) n
+        >>= fun x -> tclADD_CLEAR_IF_ID x x)
+     >>= fun (ot,clr) ->
+       if clear_if_id
+       then tclKeepOpenConstr ot >>= tclPAIR clr
+       else tclKeepOpenConstr ot >>= tclPAIR []
 
 (* we store in the state (v top), then (v1 (v2 top))... *)
-let pile_up_view (ist, v) =
+let pile_up_view ~clear_if_id (ist, v) =
   let ist = Ssrcommon.option_assert_get ist (Pp.str"not a term") in
-  State.vsPUSH (fun p -> interp_view ist v p)
+  State.vsPUSH (fun p -> interp_view ~clear_if_id ist v p)
 
 let finalize_view s0 ?(simple_types=true) p =
 Goal.enter_one ~__LOC__ begin fun g ->
@@ -292,7 +311,7 @@ let pose_proof subject_name p =
   <*>
   Tactics.New.reduce_after_refine
 
-let rec apply_all_views ending vs s0 =
+let rec apply_all_views ~clear_if_id ending vs s0 =
   match vs with
   | [] -> ending s0
   | v :: vs ->
@@ -301,31 +320,35 @@ let rec apply_all_views ending vs s0 =
       | `Tac tac ->
            Ssrprinters.ppdebug (lazy Pp.(str"..a tactic"));
            ending s0 <*> Tacinterp.eval_tactic tac <*>
-           Ssrcommon.tacSIGMA >>= apply_all_views ending vs
+           Ssrcommon.tacSIGMA >>= apply_all_views ~clear_if_id ending vs
       | `Term v ->
            Ssrprinters.ppdebug (lazy Pp.(str"..a term"));
-           pile_up_view v <*> apply_all_views ending vs s0
+           pile_up_view ~clear_if_id v <*>
+           apply_all_views ~clear_if_id ending vs s0
 
 (* Entry points *********************************************************)
 
-let tclIPAT_VIEWS ~views:vs ~conclusion:tac =
+let tclIPAT_VIEWS ~views:vs ?(clear_if_id=false) ~conclusion:tac =
   let end_view_application s0 =
-    State.vsCONSUME (fun name t ->
-      finalize_view s0 t >>= pose_proof name <*>
-      tac ~to_clear:(Option.cata (fun x -> [x]) [] name)) in
+    State.vsCONSUME (fun ~name t ~to_clear ->
+      let to_clear = Option.cata (fun x -> [x]) [] name @ to_clear in
+      finalize_view s0 t >>= pose_proof name <*> tac ~to_clear) in
   tclINDEPENDENT begin
     State.vsASSERT_EMPTY <*>
-    Ssrcommon.tacSIGMA >>= apply_all_views end_view_application vs <*>
+    Ssrcommon.tacSIGMA >>=
+      apply_all_views ~clear_if_id end_view_application vs <*>
     State.vsASSERT_EMPTY
   end
 
 let tclWITH_FWD_VIEWS ~simple_types ~subject ~views:vs ~conclusion:tac =
   let ending_tac s0 =
-    State.vsCONSUME (fun _ t -> finalize_view s0 ~simple_types t >>= tac) in
+    State.vsCONSUME (fun ~name:_ t ~to_clear:_ ->
+      finalize_view s0 ~simple_types t >>= tac) in
   tclINDEPENDENT begin
     State.vsASSERT_EMPTY <*>
-    State.vsINIT subject <*>
-    Ssrcommon.tacSIGMA >>= apply_all_views ending_tac vs <*>
+    State.vsINIT (subject,[]) <*>
+    Ssrcommon.tacSIGMA >>=
+      apply_all_views ~clear_if_id:false ending_tac vs <*>
     State.vsASSERT_EMPTY
   end
 
diff --git a/plugins/ssr/ssrview.mli b/plugins/ssr/ssrview.mli
index be51fe7f9..b128a95da 100644
--- a/plugins/ssr/ssrview.mli
+++ b/plugins/ssr/ssrview.mli
@@ -20,9 +20,11 @@ module AdaptorDb : sig
 
 end
 
-(* Apply views to the top of the stack (intro pattern) *)
+(* Apply views to the top of the stack (intro pattern). If clear_if_id is
+ * true (default false) then views that happen to be a variable are considered
+ * as to be cleared (see the to_clear argument to the continuation) *)
 val tclIPAT_VIEWS :
-    views:ast_closure_term list ->
+    views:ast_closure_term list -> ?clear_if_id:bool ->
     conclusion:(to_clear:Names.Id.t list -> unit Proofview.tactic) ->
   unit Proofview.tactic
 
diff --git a/test-suite/ssr/ipat_clear_if_id.v b/test-suite/ssr/ipat_clear_if_id.v
new file mode 100644
index 000000000..7a44db2ea
--- /dev/null
+++ b/test-suite/ssr/ipat_clear_if_id.v
@@ -0,0 +1,23 @@
+Require Import ssreflect.
+
+Axiom v1 : nat -> bool.
+
+Section Foo.
+
+Variable v2 : nat -> bool.
+
+Lemma test (v3 : nat -> bool) (v4 : bool -> bool) (v5 : bool -> bool) : nat -> nat -> nat -> nat -> True.
+Proof.
+move=> {}/v1 b1 {}/v2 b2 {}/v3 b3 {}/v2/v4/v5 b4.
+Check b1 : bool.
+Check b2 : bool.
+Check b3 : bool.
+Check b4 : bool.
+Fail Check v3.
+Fail Check v4.
+Fail Check v5.
+Check v2 : nat -> bool.
+by [].
+Qed.
+
+End Foo.