Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monad

20 files changed, 1935 insertions, 1129 deletions

diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index cdd4ee645..c53e74406 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -43,12 +43,24 @@ type ssrclear = ssrhyps
 (* Discharge occ switch (combined occurrence / clear switch) *)
 type ssrdocc = ssrclear option * ssrocc
 
-(* FIXME, make algebraic *)
-type ssrtermkind = char
-
+(* OLD ssr terms *)
+type ssrtermkind = char (* FIXME, make algebraic *)
 type ssrterm = ssrtermkind * Tacexpr.glob_constr_and_expr
 
-type ssrview = ssrterm list
+(* NEW ssr term *)
+
+(* These terms are raw but closed with the intenalization/interpretation
+ * context.  It is up to the tactic receiving it to decide if such contexts
+ * are useful or not, and eventually manipulate the term before turning it
+ * into a constr *)
+type ast_closure_term = {
+  body : Constrexpr.constr_expr;
+  glob_env : Genintern.glob_sign option; (* for Tacintern.intern_constr *)
+  interp_env :  Geninterp.interp_sign option; (* for Tacinterp.interp_open_constr_with_bindings *)
+  annotation : [ `None | `Parens | `DoubleParens | `At ];
+}
+
+type ssrview = ast_closure_term list
 
 (* TODO
 type id_mod = Hat | HatTilde | Sharp
@@ -59,7 +71,6 @@ type anon_iter =
   | One
   | Drop
   | All
-
 (* TODO
   | Dependent (* fast mode *)
   | UntilMark
@@ -71,15 +82,15 @@ type ssripat =
   | IPatId of (*TODO id_mod option * *) Id.t
   | IPatAnon of anon_iter (* inaccessible name *)
 (* TODO  | IPatClearMark *)
-(* TODO | IPatDispatch of ssripatss (* /[..|..] *) *)
+  | IPatDispatch of ssripatss (* /[..|..] *)
   | 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 ssrterm list (* /view *)
+  | IPatView of ssrview (* /view *)
   | IPatClear of ssrclear (* {H1 H2} *)
   | IPatSimpl of ssrsimpl
-  | IPatNewHidden of Id.t list
-(* | IPatVarsForAbstract of Id.t list *)
+  | IPatAbstractVars of Id.t list
+  | IPatTac of unit Proofview.tactic
 
 and ssripats = ssripat list
 and ssripatss = ssripats list
@@ -127,12 +138,12 @@ type 'tac ssrhint = bool * 'tac option list
 type 'tac fwdbinders =
         bool * (ssrhpats * ((ssrfwdfmt * ssrterm) * 'tac ssrhint))
 
-type clause = 
+type clause =
   (ssrclear * ((ssrhyp_or_id * string) *
               Ssrmatching_plugin.Ssrmatching.cpattern option) option)
 type clauses = clause list * ssrclseq
 
-type wgen = 
+type wgen =
            (ssrclear *
             ((ssrhyp_or_id * string) *
              Ssrmatching_plugin.Ssrmatching.cpattern option)
@@ -141,9 +152,20 @@ type wgen =
 type 'a ssrdoarg = ((ssrindex * ssrmmod) * 'a ssrhint) * clauses
 type 'a ssrseqarg = ssrindex * ('a ssrhint * 'a option)
 
+
+open Ssrmatching_plugin
+open Ssrmatching
+type ssrdgens = { dgens : (ssrdocc * cpattern) list;
+                  gens  : (ssrdocc * cpattern) list;
+                  clr  : ssrclear }
+type ssrcasearg = ssripat option * (ssrdgens * ssripats)
+type ssrmovearg = ssrview * ssrcasearg
+type ssragens = ((ssrhyps option * occ) * ssrterm) list list * ssrclear
+type ssrapplyarg = ssrterm list * (ssragens * ssripats)
+
 (* OOP : these are general shortcuts *)
 type gist = Tacintern.glob_sign
 type ist = Tacinterp.interp_sign
-type goal = Goal.goal 
+type goal = Goal.goal
 type 'a sigma = 'a Evd.sigma
 type v82tac = Tacmach.tactic
diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index c29a1fe7c..23da1eb69 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -51,6 +51,24 @@ let interp_agen ist gl ((goclr, _), (k, gc as c)) (clr, rcs) =
 
 let pf_pr_glob_constr gl = pr_glob_constr_env (pf_env gl)
 
+let interp_nbargs ist gl rc =
+  try
+    let rc6 = mkRApp rc (mkRHoles 6) in
+    let sigma, t = interp_open_constr ist gl (rc6, None) in
+    let si = sig_it gl in
+    let gl = re_sig si sigma in
+    6 + Ssrcommon.nbargs_open_constr gl t
+  with _ -> 5
+
+let interp_view_nbimps ist gl rc =
+  try
+    let sigma, t = interp_open_constr ist gl (rc, None) in
+    let si = sig_it gl in
+    let gl = re_sig si sigma in
+    let pl, c = splay_open_constr gl t in
+    if Ssrcommon.isAppInd (pf_env gl) (project gl) c then List.length pl else (-(List.length pl))
+  with _ -> 0
+
 let interp_agens ist gl gagens =
   match List.fold_right (interp_agen ist gl) gagens ([], []) with
   | clr, rlemma :: args ->
@@ -86,40 +104,55 @@ let mkRAppView ist gl rv gv =
 
 let prof_apply_interp_with = mk_profiler "ssrapplytac.interp_with";;
 
-let refine_interp_apply_view i ist gl gv =
+let refine_interp_apply_view dbl ist gl gv =
   let pair i = List.map (fun x -> i, x) in
   let rv = pf_intern_term ist gl gv in
   let v = mkRAppView ist gl rv gv in
-  let interp_with (i, hint) =
+  let interp_with (dbl, hint) =
+    let i = if dbl = Ssrview.AdaptorDb.Equivalence then 2 else 1 in
     interp_refine ist gl (mkRApp hint (v :: mkRHoles i)) in
   let interp_with x = prof_apply_interp_with.profile interp_with x in
   let rec loop = function
   | [] -> (try apply_rconstr ~ist rv gl with _ -> view_error "apply" gv)
   | h :: hs -> (try refine_with (snd (interp_with h)) gl with _ -> loop hs) in
-  loop (pair i Ssrview.viewtab.(i) @
-        if i = 2 then pair 1 Ssrview.viewtab.(1) else [])
-
-let apply_top_tac gl =
-  Tacticals.tclTHENLIST [introid top_id; apply_rconstr (mkRVar top_id); Proofview.V82.of_tactic (Tactics.clear [top_id])] gl
-
-let inner_ssrapplytac gviews ggenl gclr ist gl =
+  loop (pair dbl (Ssrview.AdaptorDb.get dbl) @
+        if dbl = Ssrview.AdaptorDb.Equivalence
+        then pair Ssrview.AdaptorDb.Backward (Ssrview.AdaptorDb.(get Backward))
+        else [])
+
+let apply_top_tac =
+  Tacticals.tclTHENLIST [
+    introid top_id;
+    apply_rconstr (mkRVar top_id);
+    old_cleartac [SsrHyp(None,top_id)]
+  ]
+
+let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic ~nf_evars:false (fun gl ->
  let _, clr = interp_hyps ist gl gclr in
  let vtac gv i gl' = refine_interp_apply_view i ist gl' gv in
  let ggenl, tclGENTAC =
    if gviews <> [] && ggenl <> [] then
-     let ggenl= List.map (fun (x,g) -> x, cpattern_of_term g) (List.hd ggenl) in
-     [], Tacticals.tclTHEN (genstac (ggenl,[]) ist)
+     let ggenl= List.map (fun (x,g) -> x, cpattern_of_term g ist) (List.hd ggenl) in
+     [], Tacticals.tclTHEN (genstac (ggenl,[]))
    else ggenl, Tacticals.tclTHEN Tacticals.tclIDTAC in
  tclGENTAC (fun gl ->
   match gviews, ggenl with
   | v :: tl, [] ->
-    let dbl = if List.length tl = 1 then 2 else 1 in
+    let dbl =
+      if List.length tl = 1
+      then Ssrview.AdaptorDb.Equivalence
+      else Ssrview.AdaptorDb.Backward in
     Tacticals.tclTHEN
-      (List.fold_left (fun acc v -> Tacticals.tclTHENLAST acc (vtac v dbl)) (vtac v 1) tl)
-      (cleartac clr) gl
+      (List.fold_left (fun acc v ->
+         Tacticals.tclTHENLAST acc (vtac v dbl))
+        (vtac v Ssrview.AdaptorDb.Backward) tl)
+      (old_cleartac clr) gl
   | [], [agens] ->
     let clr', (sigma, lemma) = interp_agens ist gl agens in
     let gl = pf_merge_uc_of sigma gl in
-    Tacticals.tclTHENLIST [cleartac clr; refine_with ~beta:true lemma; cleartac clr'] gl
-  | _, _ -> Tacticals.tclTHEN apply_top_tac (cleartac clr) gl) gl
+    Tacticals.tclTHENLIST [old_cleartac clr; refine_with ~beta:true lemma; old_cleartac clr'] gl
+  | _, _ ->
+     Tacticals.tclTHENLIST [apply_top_tac; old_cleartac clr] gl) gl
+)
 
+let apply_top_tac = Proofview.V82.tactic ~nf_evars:false apply_top_tac
diff --git a/plugins/ssr/ssrbwd.mli b/plugins/ssr/ssrbwd.mli
index af9f7491a..eb64f337f 100644
--- a/plugins/ssr/ssrbwd.mli
+++ b/plugins/ssr/ssrbwd.mli
@@ -6,16 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+open Ssrast
+open Proofview
 
+val apply_top_tac : unit tactic
 
-val apply_top_tac : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
-
-val inner_ssrapplytac :
-  Ssrast.ssrterm list ->
-  ((Ssrast.ssrhyps option * Ssrmatching_plugin.Ssrmatching.occ) *
-     (Ssrast.ssrtermkind * Tacexpr.glob_constr_and_expr))
-    list list ->
-  Ssrast.ssrhyps ->
-  Ssrast.ist ->
-  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
+val inner_ssrapplytac : ssrterm list -> ssragens -> ist -> unit tactic
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 1a02fb91c..48ec8166c 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -170,6 +170,11 @@ let array_list_of_tl v =
 
 (* end patch *)
 
+let option_assert_get o msg =
+  match o with
+  | None -> CErrors.anomaly msg
+  | Some x -> x
+
 
 (** Constructors for rawconstr *)
 open Glob_term
@@ -220,8 +225,9 @@ let splay_open_constr gl (sigma, c) =
   let env = pf_env gl in let t = Retyping.get_type_of env sigma c in
   Reductionops.splay_prod env sigma t
 
-let isAppInd gl c =
-  try ignore (pf_reduce_to_atomic_ind gl c); true with _ -> false
+let isAppInd env sigma c =
+  try ignore(Tacred.reduce_to_atomic_ind env sigma c); true
+  with CErrors.UserError _ -> false
 
 (** Generic argument-based globbing/typing utilities *)
 
@@ -276,30 +282,46 @@ let interp_hyps ist gl ghyps =
   let hyps = List.map snd (List.map (interp_hyp ist gl) ghyps) in
   check_hyps_uniq [] hyps; Tacmach.project gl, hyps
 
+(* Old terms *)
 let mk_term k c = k, (mkRHole, Some c)
 let mk_lterm c = mk_term xNoFlag c
 
-let interp_view_nbimps ist gl rc =
-  try
-    let sigma, t = interp_open_constr ist gl (rc, None) in
-    let si = sig_it gl in
-    let gl = re_sig si sigma in
-    let pl, c = splay_open_constr gl t in
-    if isAppInd gl c then List.length pl else (-(List.length pl))
-  with _ -> 0
+(* New terms *)
+
+let mk_ast_closure_term a t = {
+  annotation = a;
+  body = t;
+  interp_env = None;
+  glob_env = None;
+}
+
+let glob_ast_closure_term (ist : Genintern.glob_sign) t =
+  { t with glob_env = Some ist }
+let subst_ast_closure_term (_s : Mod_subst.substitution) t =
+  (* _s makes sense only for glob constr *)
+  t
+let interp_ast_closure_term (ist : Geninterp.interp_sign) (gl : 'goal Evd.sigma) t =
+  (* gl is only useful if we want to interp *now*, later we have
+   * a potentially different gl.sigma *)
+  Tacmach.project gl, { t with interp_env = Some ist }
+
+let ssrterm_of_ast_closure_term { body; annotation } =
+  let c = match annotation with
+    | `Parens -> xInParens
+    | `At -> xWithAt
+    | _ -> xNoFlag in
+  mk_term c body
+
+let ssrdgens_of_parsed_dgens = function
+  | [], clr -> { dgens = []; gens = []; clr }
+  | [gens], clr -> { dgens = []; gens; clr }
+  | [dgens;gens], clr -> { dgens; gens; clr }
+  | _ -> assert false
+
 
 let nbargs_open_constr gl oc =
   let pl, _ = splay_open_constr gl oc in List.length pl
 
-let interp_nbargs ist gl rc =
-  try
-    let rc6 = mkRApp rc (mkRHoles 6) in
-    let sigma, t = interp_open_constr ist gl (rc6, None) in
-    let si = sig_it gl in
-    let gl = re_sig si sigma in
-    6 + nbargs_open_constr gl t
-  with _ -> 5
-
 let pf_nbargs gl c = nbargs_open_constr gl (project gl, c)
 
 let internal_names = ref []
@@ -378,7 +400,7 @@ let max_suffix m (t, j0 as tj0) id  =
     dt < ds && skip_digits s i = n in
   loop m
 
-let mk_anon_id t gl =
+let mk_anon_id t gl_ids =
   let m, si0, id0 =
     let s = ref (Printf.sprintf  "_%s_" t) in
     if is_internal_name !s then s := "_" ^ !s;
@@ -387,7 +409,6 @@ let mk_anon_id t gl =
       let d = !s.[i] in if not (is_digit d) then i + 1, j else
       loop (i - 1) (if d = '0' then j else i) in
     let m, j = loop (n - 1) n in m, (!s, j), Id.of_string !s in
-  let gl_ids = pf_ids_of_hyps gl in
   if not (List.mem id0 gl_ids) then id0 else
   let s, i = List.fold_left (max_suffix m) si0 gl_ids in
   let open Bytes in
@@ -435,8 +456,8 @@ let red_product_skip_id env sigma c = match EConstr.kind sigma c with
   | App(hd,args) when Array.length args = 1 && is_id_constr sigma hd -> args.(0)
   | _ -> try Tacred.red_product env sigma c with _ -> c
 
-let ssrevaltac ist gtac =
-  Proofview.V82.of_tactic (Tacinterp.tactic_of_value ist gtac)
+let ssrevaltac ist gtac = Tacinterp.tactic_of_value ist gtac
+
 (** Open term to lambda-term coercion  {{{ ************************************)
 
 (* This operation takes a goal gl and an open term (sigma, t), and   *)
@@ -480,7 +501,7 @@ let nf_evar sigma t =
   EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr t))
 
 let pf_abs_evars2 gl rigid (sigma, c0) =
-  let c0 = EConstr.Unsafe.to_constr c0 in
+  let c0 = EConstr.to_constr sigma c0 in
   let sigma0, ucst = project gl, Evd.evar_universe_context sigma in
   let nenv = env_size (pf_env gl) in
   let abs_evar n k =
@@ -776,7 +797,7 @@ let rec is_name_in_ipats name = function
       List.exists (function SsrHyp(_,id) -> id = name) clr 
       || is_name_in_ipats name tl
   | IPatId id :: tl -> id = name || is_name_in_ipats name tl
-  | IPatCase l :: tl -> List.exists (is_name_in_ipats name) l || is_name_in_ipats name tl
+  | (IPatCase l | IPatDispatch l) :: tl -> List.exists (is_name_in_ipats name) l || is_name_in_ipats name tl
   | _ :: tl -> is_name_in_ipats name tl
   | [] -> false
 
@@ -1082,14 +1103,10 @@ let introid ?(orig=ref Anonymous) name = tclTHEN (fun gl ->
 let anontac decl gl =
   let id =  match RelDecl.get_name decl with
   | Name id ->
-    if is_discharged_id id then id else mk_anon_id (Id.to_string id) gl
-  | _ -> mk_anon_id ssr_anon_hyp gl in
+    if is_discharged_id id then id else mk_anon_id (Id.to_string id) (Tacmach.pf_ids_of_hyps gl)
+  | _ -> mk_anon_id ssr_anon_hyp (Tacmach.pf_ids_of_hyps gl) in
   introid id gl
 
-let intro_all gl =
-  let dc, _ = EConstr.decompose_prod_assum (project gl) (Tacmach.pf_concl gl) in
-  tclTHENLIST (List.map anontac (List.rev dc)) gl
-
 let rec intro_anon gl =
   try anontac (List.hd (fst (EConstr.decompose_prod_n_assum (project gl) 1 (Tacmach.pf_concl gl)))) gl
   with err0 -> try tclTHEN (Proofview.V82.of_tactic Tactics.red_in_concl) intro_anon gl with e when CErrors.noncritical e -> raise err0
@@ -1146,15 +1163,16 @@ let tclMULT = function
   | n, Must when n > 1 -> tclDO n
   | _       -> tclID
 
-let cleartac clr = check_hyps_uniq [] clr; Proofview.V82.of_tactic (Tactics.clear (hyps_ids clr))
+let old_cleartac clr = check_hyps_uniq [] clr; Proofview.V82.of_tactic (Tactics.clear (hyps_ids clr))
+let cleartac clr = check_hyps_uniq [] clr; Tactics.clear (hyps_ids clr)
 
 (** }}} *)
 
 (** Generalize tactic *)
 
 (* XXX the k of the redex should percolate out *)
-let pf_interp_gen_aux ist gl to_ind ((oclr, occ), t) =
-  let pat = interp_cpattern ist gl t None in (* UGLY API *)
+let pf_interp_gen_aux gl to_ind ((oclr, occ), t) =
+  let pat = interp_cpattern gl t None in (* UGLY API *)
   let cl, env, sigma = Tacmach.pf_concl gl, pf_env gl, project gl in
   let (c, ucst), cl = 
     try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr cl) pat occ 1
@@ -1195,22 +1213,22 @@ let genclrtac cl cs clr =
       (fun type_err gl ->
          tclTHEN
            (tclTHEN (Proofview.V82.of_tactic (Tactics.elim_type (EConstr.of_constr
-             (Universes.constr_of_global @@ Coqlib.build_coq_False ())))) (cleartac clr))
+             (Universes.constr_of_global @@ Coqlib.build_coq_False ())))) (old_cleartac clr))
            (fun gl -> raise type_err)
            gl))
-    (cleartac clr)
+    (old_cleartac clr)
 
-let gentac ist gen gl =
+let gentac gen gl =
 (*   ppdebug(lazy(str"sigma@gentac=" ++ pr_evar_map None (project gl))); *)
-  let conv, _, cl, c, clr, ucst,gl = pf_interp_gen_aux ist gl false gen in
+  let conv, _, cl, c, clr, ucst,gl = pf_interp_gen_aux gl false gen in
   ppdebug(lazy(str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c));
   let gl = pf_merge_uc ucst gl in
   if conv
-  then tclTHEN (Proofview.V82.of_tactic (convert_concl cl)) (cleartac clr) gl
+  then tclTHEN (Proofview.V82.of_tactic (convert_concl cl)) (old_cleartac clr) gl
   else genclrtac cl [c] clr gl
 
-let genstac (gens, clr) ist =
-  tclTHENLIST (cleartac clr :: List.rev_map (gentac ist) gens)
+let genstac (gens, clr) =
+  tclTHENLIST (old_cleartac clr :: List.rev_map gentac gens)
 
 let gen_tmp_ids
   ?(ist=Geninterp.({ lfun = Id.Map.empty; extra = Tacinterp.TacStore.empty })) gl
@@ -1220,13 +1238,13 @@ let gen_tmp_ids
     (tclTHENLIST
       (List.map (fun (id,orig_ref) ->
         tclTHEN 
-        (gentac ist ((None,Some(false,[])),cpattern_of_id id))
+        (gentac ((None,Some(false,[])),cpattern_of_id id))
         (rename_hd_prod orig_ref))
       ctx.tmp_ids) gl)
 ;;
 
-let pf_interp_gen ist gl to_ind gen =
-  let _, _, a, b, c, ucst,gl = pf_interp_gen_aux ist gl to_ind gen in
+let pf_interp_gen gl to_ind gen =
+  let _, _, a, b, c, ucst,gl = pf_interp_gen_aux gl to_ind gen in
   a, b ,c, pf_merge_uc ucst gl
 
 (* TASSI: This version of unprotects inlines the unfold tactic definition, 
@@ -1247,7 +1265,11 @@ let unprotecttac gl =
            CClosure.RedFlags.fCOFIX]), DEFAULTcast) hyploc))
     allHypsAndConcl gl
 
-let abs_wgen keep_let ist f gen (gl,args,c) =
+let is_protect hd env sigma =
+  let _, protectC = mkSsrConst "protect_term" env sigma in
+  EConstr.eq_constr_nounivs sigma hd protectC
+
+let abs_wgen keep_let f gen (gl,args,c) =
   let sigma, env = project gl, pf_env gl in
   let evar_closed t p =
     if occur_existential sigma t then
@@ -1267,7 +1289,7 @@ let abs_wgen keep_let ist f gen (gl,args,c) =
      gl, EConstr.mkVar x :: args, EConstr.mkProd (Name (f x),Tacmach.pf_get_hyp_typ gl x, EConstr.Vars.subst_var x c)
   | _, Some ((x, "@"), Some p) -> 
      let x = hoi_id x in
-     let cp = interp_cpattern ist gl p None in
+     let cp = interp_cpattern gl p None in
      let (t, ucst), c =
        try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr c) cp None 1
        with NoMatch -> redex_of_pattern env cp, (EConstr.Unsafe.to_constr c) in
@@ -1279,7 +1301,7 @@ let abs_wgen keep_let ist f gen (gl,args,c) =
      pf_merge_uc ucst gl, args, EConstr.mkLetIn(Name (f x), ut, ty, c)
   | _, Some ((x, _), Some p) ->
      let x = hoi_id x in
-     let cp = interp_cpattern ist gl p None in
+     let cp = interp_cpattern gl p None in
      let (t, ucst), c =
        try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr c) cp None 1
        with NoMatch -> redex_of_pattern env cp, (EConstr.Unsafe.to_constr c) in
@@ -1293,8 +1315,252 @@ let abs_wgen keep_let ist f gen (gl,args,c) =
 let clr_of_wgen gen clrs = match gen with
   | clr, Some ((x, _), None) ->
      let x = hoi_id x in
-     cleartac clr :: cleartac [SsrHyp(Loc.tag x)] :: clrs
-  | clr, _ -> cleartac clr :: clrs
+     old_cleartac clr :: old_cleartac [SsrHyp(Loc.tag x)] :: clrs
+  | clr, _ -> old_cleartac clr :: clrs
+
+
+let reduct_in_concl t = Tactics.reduct_in_concl (t, DEFAULTcast)
+let unfold cl =
+  let module R = Reductionops in let module F = CClosure.RedFlags in
+  reduct_in_concl (R.clos_norm_flags (F.mkflags
+    (List.map (fun c -> F.fCONST (fst (destConst (EConstr.Unsafe.to_constr c)))) cl @
+       [F.fBETA; F.fMATCH; F.fFIX; F.fCOFIX])))
+
+open Proofview
+open Notations
+
+let tacSIGMA = Goal.enter_one begin fun g ->
+  let k = Goal.goal g in
+  let sigma = Goal.sigma g in
+  tclUNIT (Tacmach.re_sig k sigma)
+end
+
+let tclINTERP_AST_CLOSURE_TERM_AS_CONSTR c =
+  tclINDEPENDENTL begin tacSIGMA >>= fun gl ->
+  let old_ssrterm = mkRHole, Some c.Ssrast.body in
+  let ist =
+    option_assert_get c.Ssrast.interp_env
+      Pp.(str "tclINTERP_AST_CLOSURE_TERM_AS_CONSTR: term with no ist") in
+  let sigma, t =
+    interp_wit Stdarg.wit_constr ist gl old_ssrterm in
+  Unsafe.tclEVARS sigma <*>
+  tclUNIT t
+end
+
+let tacREDUCE_TO_QUANTIFIED_IND ty =
+  tacSIGMA >>= fun gl ->
+  tclUNIT (Tacmach.pf_reduce_to_quantified_ind gl ty)
+
+let tacTYPEOF c = Goal.enter_one ~__LOC__ (fun g ->
+  let sigma, env = Goal.sigma g, Goal.env g in
+  let sigma, ty = Typing.type_of env sigma c in
+  Unsafe.tclEVARS sigma <*> tclUNIT ty)
+
+(** This tactic creates a partial proof realizing the introduction rule, but
+    does not check anything. *)
+let unsafe_intro env store decl b =
+  let open Context.Named.Declaration in
+  Refine.refine ~typecheck:false begin fun sigma ->
+    let ctx = Environ.named_context_val env in
+    let nctx = EConstr.push_named_context_val decl ctx in
+    let inst = List.map (get_id %> EConstr.mkVar) (Environ.named_context env) in
+    let ninst = EConstr.mkRel 1 :: inst in
+    let nb = EConstr.Vars.subst1 (EConstr.mkVar (get_id decl)) b in
+    let sigma, ev =
+      Evarutil.new_evar_instance nctx sigma nb ~principal:true ~store ninst in
+    sigma, EConstr.mkNamedLambda_or_LetIn decl ev
+  end
+
+let set_decl_id id = let open Context in function
+  | Rel.Declaration.LocalAssum(name,ty) -> Named.Declaration.LocalAssum(id,ty)
+  | Rel.Declaration.LocalDef(name,ty,t) -> Named.Declaration.LocalDef(id,ty,t)
+
+let rec decompose_assum env sigma orig_goal =
+  let open Context in
+  match EConstr.kind sigma orig_goal with
+  | Prod(name,ty,t) ->
+      Rel.Declaration.LocalAssum(name,ty), t, true
+  | LetIn(name,ty,t1,t2) -> Rel.Declaration.LocalDef(name, ty, t1), t2, true
+  | _ ->
+      let goal = Reductionops.whd_allnolet env sigma orig_goal in
+      match EConstr.kind sigma goal with
+      | Prod(name,ty,t) -> Rel.Declaration.LocalAssum(name,ty), t, false
+      | LetIn(name,ty,t1,t2) -> Rel.Declaration.LocalDef(name,ty,t1), t2, false
+      | App(hd,args) when EConstr.isLetIn sigma hd -> (* hack *)
+          let _,v,_,b = EConstr.destLetIn sigma hd in
+          let ctx, t, _ =
+            decompose_assum env sigma
+              (EConstr.mkApp (EConstr.Vars.subst1 v b, args)) in
+          ctx, t, false
+      | _ -> CErrors.user_err
+          Pp.(str "No assumption in " ++ Printer.pr_econstr_env env sigma goal)
+
+let tclFULL_BETAIOTA = Goal.enter begin fun gl ->
+  let r, _ = Redexpr.reduction_of_red_expr (Goal.env gl)
+    Genredexpr.(Lazy {
+      rBeta=true; rMatch=true; rFix=true; rCofix=true;
+      rZeta=false; rDelta=false; rConst=[]}) in
+  Tactics.e_reduct_in_concl ~check:false (r,Constr.DEFAULTcast)
+end
+
+(** [intro id k] introduces the first premise (product or let-in) of the goal
+    under the name [id], reducing the head of the goal (using beta, iota, delta
+    but not zeta) if necessary. If [id] is None, a name is generated, that will
+    not be user accessible. If the goal does not start with a product or a
+let-in even after reduction, it fails. In case of success, the original name
+and final id are passed to the continuation [k] which gets evaluated. *)
+let tclINTRO ~id ~conclusion:k = Goal.enter begin fun gl ->
+  let open Context in
+  let env, sigma, extra, g = Goal.(env gl, sigma gl, extra gl, concl gl) in
+  let decl, t, no_red = decompose_assum env sigma g in
+  let original_name = Rel.Declaration.get_name decl in
+  let already_used = Tacmach.New.pf_ids_of_hyps gl in
+  let id = match id, original_name with
+    | Some id, _ -> id
+    | _, Name id ->
+       if is_discharged_id id then id
+       else mk_anon_id (Id.to_string id) already_used
+    | _, _ ->
+       let ids = Tacmach.New.pf_ids_of_hyps gl in
+       mk_anon_id ssr_anon_hyp ids
+  in
+  if List.mem id already_used then
+    errorstrm Pp.(Id.print id ++ str" already used");
+  unsafe_intro env extra (set_decl_id id decl) t <*>
+  (if no_red then tclUNIT () else tclFULL_BETAIOTA) <*>
+  k ~orig_name:original_name ~new_name:id
+end
+
+let return ~orig_name:_ ~new_name:_ = tclUNIT ()
+
+let tclINTRO_ID id = tclINTRO ~id:(Some id) ~conclusion:return
+let tclINTRO_ANON = tclINTRO ~id:None ~conclusion:return
+
+let tclRENAME_HD_PROD name = Goal.enter begin fun gl ->
+  let convert_concl_no_check t =
+    Tactics.convert_concl_no_check t Term.DEFAULTcast in
+  let concl = Goal.concl gl in
+  let sigma = Goal.sigma gl in
+  match EConstr.kind sigma concl with
+  | Prod(_,src,tgt) ->
+      convert_concl_no_check EConstr.(mkProd (name,src,tgt))
+  | _ -> CErrors.anomaly (Pp.str "rename_hd_prod: no head product")
+end
+
+let tcl0G tac =
+  numgoals >>= fun ng -> if ng = 0 then tclUNIT () else tac
+
+let rec tclFIRSTa = function
+  | [] -> Tacticals.New.tclZEROMSG Pp.(str"No applicable tactic.")
+  | tac :: rest -> tclORELSE tac (fun _ -> tclFIRSTa rest)
+
+let rec tclFIRSTi tac n =
+  if n < 0 then Tacticals.New.tclZEROMSG Pp.(str "tclFIRSTi")
+  else tclORELSE (tclFIRSTi tac (n-1)) (fun _ -> tac n)
+
+let tacCONSTR_NAME ?name c =
+  match name with
+  | Some n -> tclUNIT n
+  | None ->
+      Goal.enter_one ~__LOC__ (fun g ->
+        let sigma = Goal.sigma g in
+        tclUNIT (constr_name sigma c))
+
+let tacMKPROD c ?name cl =
+  tacTYPEOF c >>= fun t ->
+  tacCONSTR_NAME ?name c >>= fun name ->
+  Goal.enter_one ~__LOC__ begin fun g ->
+    let sigma, env = Goal.sigma g, Goal.env g in
+    if name <> Names.Name.Anonymous || EConstr.Vars.noccurn sigma  1 cl
+    then tclUNIT (EConstr.mkProd (name, t, cl))
+    else
+      let name = Names.Id.of_string (Namegen.hdchar env sigma t) in
+      tclUNIT (EConstr.mkProd (Names.Name.Name name, t, cl))
+end
+
+let tacINTERP_CPATTERN cp =
+  tacSIGMA >>= begin fun gl ->
+  tclUNIT (Ssrmatching.interp_cpattern gl cp None)
+end
+
+let tacUNIFY a b =
+  tacSIGMA >>= begin fun gl ->
+  let gl = Ssrmatching.pf_unify_HO gl a b in
+  Unsafe.tclEVARS (Tacmach.project gl)
+end
+
+let tclOPTION o d =
+  match o with
+  | None -> d >>= tclUNIT
+  | Some x -> tclUNIT x
+
+let tacIS_INJECTION_CASE ?ty t = begin
+  tclOPTION ty (tacTYPEOF t) >>= fun ty ->
+  tacREDUCE_TO_QUANTIFIED_IND ty >>= fun ((mind,_),_) ->
+  tclUNIT (Globnames.eq_gr (Globnames.IndRef mind) (Coqlib.build_coq_eq ()))
+end
+
+let tclWITHTOP tac = Goal.enter begin fun gl ->
+  let top =
+    mk_anon_id "top_assumption" (Tacmach.New.pf_ids_of_hyps gl) in
+  tclINTRO_ID top <*>
+  tac (EConstr.mkVar top) <*>
+  Tactics.clear [top]
+end
+
+let tacMK_SSR_CONST name = Goal.enter_one ~__LOC__ begin fun g ->
+  let sigma, env = Goal.(sigma g, env g) in
+  let sigma, c = mkSsrConst name env sigma in
+  Unsafe.tclEVARS sigma <*>
+  tclUNIT c
+end
+
+module type StateType = sig
+  type state
+  val init : state
+end
+
+module MakeState(S : StateType) = struct
+
+let state_field : S.state Proofview_monad.StateStore.field =
+  Proofview_monad.StateStore.field ()
+
+(* FIXME: should not inject fresh_state, but initialize it at the beginning *)
+let lift_upd_state upd s =
+  let open Proofview_monad.StateStore in
+  let old_state = Option.default S.init (get s state_field) in
+  upd old_state >>= fun new_state ->
+  tclUNIT (set s state_field new_state)
+
+let tacUPDATE upd = Goal.enter begin fun gl ->
+  let s0 = Goal.state gl in
+  Goal.enter_one ~__LOC__ (fun _ -> lift_upd_state upd s0) >>= fun s ->
+  Unsafe.tclGETGOALS >>= fun gls ->
+  let gls = List.map (fun gs ->
+    let g = Proofview_monad.drop_state gs in
+    Proofview_monad.goal_with_state g s) gls in
+  Unsafe.tclSETGOALS gls
+end
+
+let tclGET k = Goal.enter begin fun gl ->
+  let open Proofview_monad.StateStore in
+  k (Option.default S.init (get (Goal.state gl) state_field))
+end
+
+let tclSET new_s =
+  let open Proofview_monad.StateStore in
+  Unsafe.tclGETGOALS >>= fun gls ->
+  let gls = List.map (fun gs ->
+    let g = Proofview_monad.drop_state gs in
+    let s = Proofview_monad.get_state gs in
+    Proofview_monad.goal_with_state g (set s state_field new_s)) gls in
+  Unsafe.tclSETGOALS gls
+
+let get g =
+  Option.default S.init
+    (Proofview_monad.StateStore.get (Goal.state g) state_field)
+
+end
 
 
 (* vim: set filetype=ocaml foldmethod=marker: *)
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index c39945194..016e331ad 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -18,6 +18,8 @@ open Ssrast
 open Ltac_plugin
 open Genarg
 
+open Ssrmatching_plugin
+
 val allocc : ssrocc
 
 (******************************** hyps ************************************)
@@ -48,6 +50,8 @@ val array_app_tl : 'a array -> 'a list -> 'a list
 val array_list_of_tl : 'a array -> 'a list
 val array_fold_right_from : int -> ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
 
+val option_assert_get : 'a option -> Pp.t -> 'a
+
 (**************************** lifted tactics ******************************)
 
 (* tactics with extra data attached to each goals, e.g. the list of
@@ -150,17 +154,22 @@ val splay_open_constr :
            Goal.goal Evd.sigma ->
            evar_map * EConstr.t ->
            (Names.Name.t * EConstr.t) list * EConstr.t
-val isAppInd : Goal.goal Evd.sigma -> EConstr.types -> bool
-val interp_view_nbimps :
-           Tacinterp.interp_sign ->
-           Goal.goal Evd.sigma -> Glob_term.glob_constr -> int
-val interp_nbargs :
-           Tacinterp.interp_sign ->
-           Goal.goal Evd.sigma -> Glob_term.glob_constr -> int
+val isAppInd : Environ.env -> Evd.evar_map -> EConstr.types -> bool
 
+val mk_term : ssrtermkind -> constr_expr -> ssrterm
+val mk_lterm : constr_expr -> ssrterm
 
-val mk_term : ssrtermkind -> 'b -> ssrtermkind * (Glob_term.glob_constr * 'b option)
-val mk_lterm : 'a -> ssrtermkind * (Glob_term.glob_constr * 'a option)
+val mk_ast_closure_term :
+  [ `None | `Parens | `DoubleParens | `At ] ->
+  Constrexpr.constr_expr -> ast_closure_term
+val interp_ast_closure_term : Geninterp.interp_sign -> Proof_type.goal
+Evd.sigma -> ast_closure_term -> Evd.evar_map * ast_closure_term
+val subst_ast_closure_term : Mod_subst.substitution -> ast_closure_term -> ast_closure_term
+val glob_ast_closure_term : Genintern.glob_sign -> ast_closure_term -> ast_closure_term
+val ssrterm_of_ast_closure_term : ast_closure_term -> ssrterm
+
+val ssrdgens_of_parsed_dgens :
+  (ssrdocc * Ssrmatching.cpattern) list list * ssrclear -> ssrdgens
 
 val is_internal_name : string -> bool
 val add_internal_name : (string -> bool) -> unit
@@ -199,11 +208,6 @@ val pf_abs_prod :
            Goal.goal Evd.sigma ->
            EConstr.t ->
            EConstr.t -> Goal.goal Evd.sigma * EConstr.types
-val pf_mkprod :
-           Goal.goal Evd.sigma ->
-           EConstr.t ->
-           ?name:Name.t ->
-           EConstr.t -> Goal.goal Evd.sigma * EConstr.types
 
 val mkSsrRRef : string -> Glob_term.glob_constr * 'a option
 val mkSsrRef : string -> Globnames.global_reference
@@ -229,17 +233,19 @@ val has_discharged_tag : string -> bool
 val ssrqid : string -> Libnames.qualid 
 val new_tmp_id :
   tac_ctx -> (Names.Id.t * Name.t ref) * tac_ctx
-val mk_anon_id : string -> Goal.goal Evd.sigma -> Id.t
+val mk_anon_id : string -> Id.t list -> Id.t
 val pf_abs_evars_pirrel :
            Goal.goal Evd.sigma ->
            evar_map * Constr.constr -> int * Constr.constr
+val nbargs_open_constr : Goal.goal Evd.sigma -> Evd.evar_map * EConstr.t -> int
 val pf_nbargs : Goal.goal Evd.sigma -> EConstr.t -> int
 val gen_tmp_ids : 
            ?ist:Geninterp.interp_sign ->
            (Goal.goal * tac_ctx) Evd.sigma ->
            (Goal.goal * tac_ctx) list Evd.sigma
 
-val ssrevaltac : Tacinterp.interp_sign -> Tacinterp.Value.t -> Proofview.V82.tac
+val ssrevaltac :
+  Tacinterp.interp_sign -> Tacinterp.Value.t -> unit Proofview.tactic
 
 val convert_concl_no_check : EConstr.t -> unit Proofview.tactic
 val convert_concl : EConstr.t -> unit Proofview.tactic
@@ -334,33 +340,29 @@ val rewritetac : ssrdir -> EConstr.t -> tactic
 
 type name_hint = (int * EConstr.types array) option ref
 
-val gentac : 
-  (Geninterp.interp_sign ->
-   (Ssrast.ssrdocc) *
-     Ssrmatching_plugin.Ssrmatching.cpattern -> Tacmach.tactic)
+val gentac :
+   Ssrast.ssrdocc * Ssrmatching.cpattern -> v82tac
 
 val genstac :
-  ((Ssrast.ssrhyp list option * Ssrmatching_plugin.Ssrmatching.occ) *
-     Ssrmatching_plugin.Ssrmatching.cpattern)
+  ((Ssrast.ssrhyp list option * Ssrmatching.occ) *
+     Ssrmatching.cpattern)
     list * Ssrast.ssrhyp list ->
-  Tacinterp.interp_sign -> Tacmach.tactic
+  Tacmach.tactic
 
 val pf_interp_gen :
-  Tacinterp.interp_sign ->
   Goal.goal Evd.sigma ->
   bool ->
-  (Ssrast.ssrhyp list option * Ssrmatching_plugin.Ssrmatching.occ) *
-    Ssrmatching_plugin.Ssrmatching.cpattern ->
+  (Ssrast.ssrhyp list option * Ssrmatching.occ) *
+    Ssrmatching.cpattern ->
   EConstr.t * EConstr.t * Ssrast.ssrhyp list *
     Goal.goal Evd.sigma
 
 val pf_interp_gen_aux :
-  Tacinterp.interp_sign ->
   Goal.goal Evd.sigma ->
   bool ->
-  (Ssrast.ssrhyp list option * Ssrmatching_plugin.Ssrmatching.occ) *
-    Ssrmatching_plugin.Ssrmatching.cpattern ->
-  bool * Ssrmatching_plugin.Ssrmatching.pattern * EConstr.t *
+  (Ssrast.ssrhyp list option * Ssrmatching.occ) *
+    Ssrmatching.cpattern ->
+  bool * Ssrmatching.pattern * EConstr.t *
     EConstr.t * Ssrast.ssrhyp list * UState.t *
       Goal.goal Evd.sigma
 
@@ -378,7 +380,6 @@ val mk_profiler : string -> profiler
 
 val introid : ?orig:Name.t ref -> Id.t -> v82tac
 val intro_anon : v82tac
-val intro_all : v82tac
 
 val interp_clr :
   evar_map -> ssrhyps option * (ssrtermkind * EConstr.t) -> ssrhyps
@@ -386,19 +387,20 @@ val interp_clr :
 val genclrtac :
   EConstr.constr ->
   EConstr.constr list -> Ssrast.ssrhyp list -> Tacmach.tactic
-val cleartac : ssrhyps -> v82tac
+val old_cleartac : ssrhyps -> v82tac
+val cleartac : ssrhyps -> unit Proofview.tactic
 
 val tclMULT : int * ssrmmod -> Tacmach.tactic -> Tacmach.tactic
 
 val unprotecttac : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
+val is_protect : EConstr.t -> Environ.env -> Evd.evar_map -> bool
 
 val abs_wgen :
   bool ->
-  Tacinterp.interp_sign ->
   (Id.t -> Id.t) ->
   'a *
     ((Ssrast.ssrhyp_or_id * string) *
-       Ssrmatching_plugin.Ssrmatching.cpattern option)
+       Ssrmatching.cpattern option)
       option ->
   Goal.goal Evd.sigma * EConstr.t list * EConstr.t ->
   Goal.goal Evd.sigma * EConstr.t list * EConstr.t
@@ -408,3 +410,69 @@ val clr_of_wgen :
   Proofview.V82.tac list -> Proofview.V82.tac list
 
 
+val unfold : EConstr.t list -> unit Proofview.tactic
+
+(* New code ****************************************************************)
+
+(* To call old code *)
+val tacSIGMA : Goal.goal Evd.sigma Proofview.tactic
+
+val tclINTERP_AST_CLOSURE_TERM_AS_CONSTR :
+  ast_closure_term -> EConstr.t list Proofview.tactic
+
+val tacREDUCE_TO_QUANTIFIED_IND :
+  EConstr.types ->
+    ((Names.inductive * EConstr.EInstance.t) * EConstr.types) Proofview.tactic
+
+val tacTYPEOF : EConstr.t -> EConstr.types Proofview.tactic
+
+val tclINTRO_ID : Id.t -> unit Proofview.tactic
+val tclINTRO_ANON : unit Proofview.tactic
+
+(* Lower level API, calls conclusion with the name taken from the prod *)
+val tclINTRO :
+  id:Id.t option ->
+  conclusion:(orig_name:Name.t -> new_name:Id.t -> unit Proofview.tactic) ->
+  unit Proofview.tactic
+
+val tclRENAME_HD_PROD : Name.t -> unit Proofview.tactic
+
+(* calls the tactic only if there are more than 0 goals *)
+val tcl0G : unit Proofview.tactic -> unit Proofview.tactic
+
+(* like tclFIRST but with 'a tactic *)
+val tclFIRSTa : 'a Proofview.tactic list -> 'a Proofview.tactic
+val tclFIRSTi : (int -> 'a Proofview.tactic) -> int -> 'a Proofview.tactic
+
+val tacCONSTR_NAME : ?name:Name.t -> EConstr.t -> Name.t Proofview.tactic
+
+(* [tacMKPROD t name ctx] (where ctx is a term possibly containing an unbound
+ * Rel 1) builds [forall name : ty_t, ctx] *)
+val tacMKPROD :
+  EConstr.t -> ?name:Name.t -> EConstr.types -> EConstr.types Proofview.tactic
+
+val tacINTERP_CPATTERN : Ssrmatching.cpattern -> Ssrmatching.pattern Proofview.tactic
+val tacUNIFY : EConstr.t -> EConstr.t -> unit Proofview.tactic
+
+(* if [(t : eq _ _ _)] then we can inject it *)
+val tacIS_INJECTION_CASE : ?ty:EConstr.types -> EConstr.t -> bool Proofview.tactic
+
+(** 1 shot, hands-on the top of the stack, eg for [=> ->] *)
+val tclWITHTOP : (EConstr.t -> unit Proofview.tactic) -> unit Proofview.tactic
+
+val tacMK_SSR_CONST : string -> EConstr.t Proofview.tactic
+
+module type StateType = sig
+  type state
+  val init : state
+end
+
+module MakeState(S : StateType) : sig
+
+  val tclGET : (S.state -> unit Proofview.tactic) -> unit Proofview.tactic
+  val tclSET : S.state -> unit Proofview.tactic
+  val tacUPDATE : (S.state -> S.state Proofview.tactic) -> unit Proofview.tactic
+
+  val get : Proofview.Goal.t -> S.state
+
+end
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 5782a7621..a5d44d925 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -97,20 +97,18 @@ let subgoals_tys sigma (relctx, concl) =
  *    generalize the equality in case eqid is not None
  * 4. build the tactic handle intructions and clears as required in ipats and
  *    by eqid *)
-let ssrelim ?(ind=ref None) ?(is_case=false) ?ist deps what ?elim eqid elim_intro_tac gl =
+let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac gl =
   (* some sanity checks *)
   let oc, orig_clr, occ, c_gen, gl = match what with
   | `EConstr(_,_,t) when EConstr.isEvar (project gl) t ->
     anomaly "elim called on a constr evar"
-  | `EGen _ when ist = None ->
-    anomaly "no ist and non simple elimination"
   | `EGen (_, g) when elim = None && is_wildcard g ->
        errorstrm Pp.(str"Indeterminate pattern and no eliminator")
   | `EGen ((Some clr,occ), g) when is_wildcard g ->
        None, clr, occ, None, gl
   | `EGen ((None, occ), g) when is_wildcard g -> None,[],occ,None,gl
   | `EGen ((_, occ), p as gen) ->
-       let _, c, clr,gl = pf_interp_gen (Option.get ist) gl true gen in
+       let _, c, clr,gl = pf_interp_gen gl true gen in
        Some c, clr, occ, Some p,gl
   | `EConstr (clr, occ, c) -> Some c, clr, occ, None,gl in
   let orig_gl, concl, env = gl, pf_concl gl, pf_env gl in
@@ -160,7 +158,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) ?ist deps what ?elim eqid elim_intr
         else
           let c = Option.get oc in let gl, c_ty = pfe_type_of gl c in
           let pc = match c_gen with
-            | Some p -> interp_cpattern (Option.get ist) orig_gl p None 
+            | Some p -> interp_cpattern orig_gl p None
             | _ -> mkTpat gl c in
           Some(c, c_ty, pc), gl in
       cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl
@@ -194,7 +192,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) ?ist deps what ?elim eqid elim_intr
         pf_saturate ~beta:is_case gl elim ~ty:elimty n_elim_args in
       let pred = List.assoc pred_id elim_args in
       let pc = match n_c_args, c_gen with
-        | 0, Some p -> interp_cpattern (Option.get ist) orig_gl p None 
+        | 0, Some p -> interp_cpattern orig_gl p None
         | _ -> mkTpat gl c in
       let cty = Some (c, c_ty, pc) in
       let elimty = Reductionops.whd_all env (project gl) elimty in
@@ -252,8 +250,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) ?ist deps what ?elim eqid elim_intr
     let rec loop patterns clr i = function
       | [],[] -> patterns, clr, gl
       | ((oclr, occ), t):: deps, inf_t :: inf_deps ->
-          let ist = match ist with Some x -> x | None -> assert false in
-          let p = interp_cpattern ist orig_gl t None in
+          let p = interp_cpattern orig_gl t None in
           let clr_t =
             interp_clr (project gl) (oclr,(tag_of_cpattern t,EConstr.of_constr (fst (redex_of_pattern env p)))) in
           (* if we are the index for the equation we do not clear *)
@@ -374,12 +371,14 @@ let ssrelim ?(ind=ref None) ?(is_case=false) ?ist deps what ?elim eqid elim_intr
   (* the elim tactic, with the eliminator and the predicated we computed *)
   let elim = project gl, elim in 
   let elim_tac gl =
-    Tacticals.tclTHENLIST [refine_with ~with_evars:false elim; cleartac clr] gl in
-  Tacticals.tclTHENLIST [gen_eq_tac; elim_intro_tac ?ist what eqid elim_tac is_rec clr] orig_gl
+    Tacticals.tclTHENLIST [refine_with ~with_evars:false elim; old_cleartac clr] gl in
+  Tacticals.tclTHENLIST [gen_eq_tac; elim_intro_tac what eqid elim_tac is_rec clr] orig_gl
 
 let no_intro ?ist what eqid elim_tac is_rec clr = elim_tac
 
-let elimtac x = ssrelim ~is_case:false [] (`EConstr ([],None,x)) None no_intro
+let elimtac x =
+  Proofview.V82.tactic ~nf_evars:false
+    (ssrelim ~is_case:false [] (`EConstr ([],None,x)) None no_intro)
 let casetac x = ssrelim ~is_case:true [] (`EConstr ([],None,x)) None no_intro
 
 let pf_nb_prod gl = nb_prod (project gl) (pf_concl gl)
@@ -436,6 +435,9 @@ let perform_injection c gl =
   let injtac = Tacticals.tclTHEN (introid id) (injectidl2rtac id id_with_ebind) in 
   Tacticals.tclTHENLAST (Proofview.V82.of_tactic (Tactics.apply (EConstr.compose_lam dc cl1))) injtac gl
 
-let ssrscasetac force_inj c gl =
-  if force_inj || is_injection_case c gl then perform_injection c gl
-  else casetac c gl
+let ssrscase_or_inj_tac c = Proofview.V82.tactic ~nf_evars:false (fun gl ->
+  if is_injection_case c gl then perform_injection c gl
+  else casetac c gl)
+
+let ssrscasetac c =
+  Proofview.V82.tactic ~nf_evars:false (fun gl -> casetac c gl)
diff --git a/plugins/ssr/ssrelim.mli b/plugins/ssr/ssrelim.mli
index 66e202b48..0541a13ed 100644
--- a/plugins/ssr/ssrelim.mli
+++ b/plugins/ssr/ssrelim.mli
@@ -13,7 +13,6 @@ open Ssrmatching_plugin
 val ssrelim :
   ?ind:(int * EConstr.types array) option ref ->
   ?is_case:bool ->
-  ?ist:Ltac_plugin.Tacinterp.interp_sign ->
   ((Ssrast.ssrhyps option * Ssrast.ssrocc) *
      Ssrmatching.cpattern)
     list ->
@@ -28,16 +27,14 @@ val ssrelim :
    as 'a) ->
   ?elim:EConstr.constr ->
   Ssrast.ssripat option ->
-  (?ist:Ltac_plugin.Tacinterp.interp_sign ->
-   'a ->
+  ( 'a ->
    Ssrast.ssripat option ->
    (Goal.goal Evd.sigma -> Goal.goal list Evd.sigma) ->
    bool -> Ssrast.ssrhyp list -> Tacmach.tactic) ->
   Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
-val elimtac :
-  EConstr.constr ->
-  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
+val elimtac : EConstr.constr -> unit Proofview.tactic
+
 val casetac :
   EConstr.constr ->
   Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
@@ -48,6 +45,9 @@ val perform_injection :
   Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
 val ssrscasetac :
-  bool ->
   EConstr.constr ->
-  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
+  unit Proofview.tactic
+
+val ssrscase_or_inj_tac :
+  EConstr.constr ->
+  unit Proofview.tactic
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 11ebe4337..18ada1c5d 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -617,20 +617,20 @@ let ipat_rewrite occ dir c gl = rwrxtac occ None dir (project gl, c) gl
 
 let rwargtac ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl =
   let fail = ref false in
-  let interp_rpattern ist gl gc =
-    try interp_rpattern ist gl gc
+  let interp_rpattern gl gc =
+    try interp_rpattern gl gc
     with _ when snd mult = May -> fail := true; project gl, T mkProp in
   let interp gc gl =
     try interp_term ist gl gc
     with _ when snd mult = May -> fail := true; (project gl, EConstr.mkProp) in
   let rwtac gl = 
-    let rx = Option.map (interp_rpattern ist gl) grx in
+    let rx = Option.map (interp_rpattern gl) grx in
     let t = interp gt gl in
     (match kind with
     | RWred sim -> simplintac occ rx sim
     | RWdef -> if dir = R2L then foldtac occ rx t else unfoldintac occ rx t gt
     | RWeq -> rwrxtac occ rx dir t) gl in
-  let ctac = cleartac (interp_clr (project gl) (oclr, (fst gt, snd (interp gt gl)))) in
+  let ctac = old_cleartac (interp_clr (project gl) (oclr, (fst gt, snd (interp gt gl)))) in
   if !fail then ctac gl else tclTHEN (tclMULT mult rwtac) ctac gl
 
 (** Rewrite argument sequence *)
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 5c1b399a8..d6489e728 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -27,12 +27,19 @@ module RelDecl = Context.Rel.Declaration
 let settac id c = Tactics.letin_tac None (Name id) c None
 let posetac id cl = Proofview.V82.of_tactic (settac id cl Locusops.nowhere)
 
-let ssrposetac ist (id, (_, t)) gl =
+let ssrposetac (id, (_, t)) gl =
+  let ist, t =
+    match t.Ssrast.interp_env with
+    | Some ist -> ist, Ssrcommon.ssrterm_of_ast_closure_term t
+    | None -> assert false in
   let sigma, t, ucst, _ = pf_abs_ssrterm ist gl t in
   posetac id t (pf_merge_uc ucst gl)
 
-let ssrsettac ist id ((_, (pat, pty)), (_, occ)) gl =
-  let pat = interp_cpattern ist gl pat (Option.map snd pty) in
+let ssrsettac id ((_, (pat, pty)), (_, occ)) gl =
+  let pty = Option.map (fun { Ssrast.body; interp_env } ->
+    let ist = Option.get interp_env in
+    (mkRHole, Some body), ist) pty in
+  let pat = interp_cpattern gl pat pty in
   let cl, sigma, env = pf_concl gl, project gl, pf_env gl in
   let (c, ucst), cl = 
     let cl = EConstr.Unsafe.to_constr cl in
@@ -52,57 +59,8 @@ let ssrsettac ist id ((_, (pat, pty)), (_, occ)) gl =
 
 open Util
 
-let rec is_Evar_or_CastedMeta sigma x =
-  EConstr.isEvar sigma x || EConstr.isMeta sigma x ||
-  (EConstr.isCast sigma x && is_Evar_or_CastedMeta sigma (pi1 (EConstr.destCast sigma x)))
-
-let occur_existential_or_casted_meta c =
-  let rec occrec c = match Constr.kind c with
-    | Evar _ -> raise Not_found
-    | Cast (m,_,_) when isMeta m -> raise Not_found
-    | _ -> Constr.iter occrec c
-  in try occrec c; false with Not_found -> true
-
 open Printer
 
-let examine_abstract id gl =
-  let gl, tid = pfe_type_of gl id in
-  let abstract, gl = pf_mkSsrConst "abstract" gl in
-  let sigma = project gl in
-  let env = pf_env gl in
-  if not (EConstr.isApp sigma tid) || not (EConstr.eq_constr sigma (fst(EConstr.destApp sigma tid)) abstract) then
-    errorstrm(strbrk"not an abstract constant: "++ pr_econstr_env env sigma id);
-  let _, args_id = EConstr.destApp sigma tid in
-  if Array.length args_id <> 3 then
-    errorstrm(strbrk"not a proper abstract constant: "++ pr_econstr_env env sigma id);
-  if not (is_Evar_or_CastedMeta sigma args_id.(2)) then
-    errorstrm(strbrk"abstract constant "++ pr_econstr_env env sigma id++str" already used");
-  tid, args_id
-
-let pf_find_abstract_proof check_lock gl abstract_n = 
-  let fire gl t = EConstr.Unsafe.to_constr (Reductionops.nf_evar (project gl) (EConstr.of_constr t)) in
-  let abstract, gl = pf_mkSsrConst "abstract" gl in
-  let l = Evd.fold_undefined (fun e ei l ->
-    match Constr.kind ei.Evd.evar_concl with
-    | App(hd, [|ty; n; lock|])
-      when (not check_lock || 
-                 (occur_existential_or_casted_meta  (fire gl ty) &&
-                  is_Evar_or_CastedMeta (project gl) (EConstr.of_constr @@ fire gl lock))) &&
-      Constr.equal hd (EConstr.Unsafe.to_constr abstract) && Constr.equal n abstract_n -> e::l
-    | _ -> l) (project gl) [] in
-  match l with
-  | [e] -> e
-  | _ -> errorstrm(strbrk"abstract constant "++ pr_constr_env (pf_env gl) (project gl) abstract_n ++
-           strbrk" not found in the evar map exactly once. "++
-           strbrk"Did you tamper with it?")
-
-let reduct_in_concl t = Tactics.reduct_in_concl (t, DEFAULTcast)
-let unfold cl =
-  let module R = Reductionops in let module F = CClosure.RedFlags in
-  reduct_in_concl (R.clos_norm_flags (F.mkflags
-    (List.map (fun c -> F.fCONST (fst (destConst (EConstr.Unsafe.to_constr c)))) cl @
-       [F.fBETA; F.fMATCH; F.fFIX; F.fCOFIX])))
-
 open Ssrast
 open Ssripats
 
@@ -140,21 +98,23 @@ let basecuttac name c gl =
   let gl, _ = pf_e_type_of gl t in
   Proofview.V82.of_tactic (Tactics.apply t) gl
 
+let introstac ipats = Proofview.V82.of_tactic (tclIPAT ipats)
+
 let havetac ist
   (transp,((((clr, pats), binders), simpl), (((fk, _), t), hint)))
   suff namefst gl 
 =
  let concl = pf_concl gl in
  let skols, pats =
-   List.partition (function IPatNewHidden _ -> true | _ -> false) pats in
- let itac_mkabs = introstac ~ist skols in
- let itac_c = introstac ~ist (IPatClear clr :: pats) in
- let itac, id, clr = introstac ~ist pats, Tacticals.tclIDTAC, cleartac clr in
+   List.partition (function IPatAbstractVars _ -> true | _ -> false) pats in
+ let itac_mkabs = introstac skols in
+ let itac_c = introstac (IPatClear clr :: pats) in
+ let itac, id, clr = introstac pats, Tacticals.tclIDTAC, old_cleartac clr in
  let binderstac n =
    let rec aux = function 0 -> [] | n -> IPatAnon One :: aux (n-1) in
-   Tacticals.tclTHEN (if binders <> [] then introstac ~ist (aux n) else Tacticals.tclIDTAC)
-     (introstac ~ist binders) in
- let simpltac = introstac ~ist simpl in
+   Tacticals.tclTHEN (if binders <> [] then introstac (aux n) else Tacticals.tclIDTAC)
+     (introstac binders) in
+ let simpltac = introstac simpl in
  let fixtc =
    not !ssrhaveNOtcresolution &&
    match fk with FwdHint(_,true) -> false | _ -> true in
@@ -178,7 +138,7 @@ let havetac ist
   let interp_ty gl rtc t =
     let a,b,_,u = pf_interp_ty ~resolve_typeclasses:rtc ist gl t in a,b,u in
   let open CAst in
-  let ct, cty, hole, loc = match t with
+  let ct, cty, hole, loc = match Ssrcommon.ssrterm_of_ast_closure_term t with
     | _, (_, Some { loc; v = CCast (ct, CastConv cty)}) ->
       mkt ct, mkt cty, mkt (mkCHole None), loc
     | _, (_, Some ct) ->
@@ -207,10 +167,10 @@ 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
-       | IPatNewHidden ids -> ids
+       | IPatAbstractVars ids -> ids
        | _ -> assert false) skols) in
      let skols_args =
-       List.map (fun id -> examine_abstract (EConstr.mkVar id) gl) skols in
+       List.map (fun id -> Ssripats.Internal.examine_abstract (EConstr.mkVar id) gl) skols in
      let gl = List.fold_right unlock_abs skols_args gl in
      let sigma, t, uc, n_evars =
        interp gl false (combineCG ct cty (mkCCast ?loc) mkRCast) in
@@ -221,7 +181,7 @@ let havetac ist
      let gl = re_sig (sig_it gl) (Evd.merge_universe_context sigma uc) in
      let gs =
        List.map (fun (_,a) ->
-         pf_find_abstract_proof false gl (EConstr.Unsafe.to_constr a.(1))) skols_args in
+         Ssripats.Internal.pf_find_abstract_proof false gl (EConstr.Unsafe.to_constr a.(1))) skols_args in
      let tacopen_skols gl =
         let stuff, g = Refiner.unpackage gl in
         Refiner.repackage stuff (gs @ [g]) in
@@ -245,75 +205,6 @@ let havetac ist
  gl
 ;;
 
-(* to extend the abstract value one needs:
-  Utility lemma to partially instantiate an abstract constant type.
-  Lemma use_abstract T n l (x : abstract T n l) : T.
-  Proof. by case: l x. Qed.
-*)
-let ssrabstract ist gens (*last*) gl =
-  let main _ (_,cid) ist gl =
-(*
-    let proj1, proj2, prod =
-      let pdata = build_prod () in
-      pdata.Coqlib.proj1, pdata.Coqlib.proj2, pdata.Coqlib.typ in
-*)
-    let concl, env = pf_concl gl, pf_env gl in
-    let fire gl t = Reductionops.nf_evar (project gl) t in
-    let abstract, gl = pf_mkSsrConst "abstract" gl in
-    let abstract_key, gl = pf_mkSsrConst "abstract_key" gl in
-    let cid_interpreted = interp_cpattern ist gl cid None in
-    let id = EConstr.mkVar (Option.get (id_of_pattern cid_interpreted)) in
-    let idty, args_id = examine_abstract id gl in
-    let abstract_n = args_id.(1) in
-    let abstract_proof = pf_find_abstract_proof true gl (EConstr.Unsafe.to_constr abstract_n) in 
-    let gl, proof =
-      let pf_unify_HO gl a b =
-        try pf_unify_HO gl a b
-        with _ -> errorstrm(strbrk"The abstract variable "++ pr_econstr_env env (project gl) id++
-          strbrk" cannot abstract this goal.  Did you generalize it?") in
-      let find_hole p t =
-        match EConstr.kind (project gl) t with
-        | Evar _ (*when last*) -> pf_unify_HO gl concl t, p
-        | Meta _ (*when last*) -> pf_unify_HO gl concl t, p
-        | Cast(m,_,_) when EConstr.isEvar (project gl) m || EConstr.isMeta
-          (project gl) m (*when last*) -> pf_unify_HO gl concl t, p
-(*
-        | Evar _ ->
-            let sigma, it = project gl, sig_it gl in
-            let sigma, ty = Evarutil.new_type_evar sigma env in
-            let gl = re_sig it sigma in
-            let p = mkApp (proj2,[|ty;concl;p|]) in
-            let concl = mkApp(prod,[|ty; concl|]) in
-            pf_unify_HO gl concl t, p
-        | App(hd, [|left; right|]) when Term.Constr.equal hd prod ->
-            find_hole (mkApp (proj1,[|left;right;p|])) left
-*)
-        | _ -> errorstrm(strbrk"abstract constant "++ pr_econstr_env env (project gl) abstract_n++
-               strbrk" has an unexpected shape. Did you tamper with it?")
-      in
-        find_hole
-          ((*if last then*) id
-          (*else mkApp(mkSsrConst "use_abstract",Array.append args_id [|id|])*))
-          (fire gl args_id.(0)) in
-    let gl = (*if last then*) pf_unify_HO gl abstract_key args_id.(2) (*else gl*) in
-    let gl, _ = pf_e_type_of gl idty in
-    let proof = fire gl proof in
-(*     if last then *)
-      let tacopen gl =
-        let stuff, g = Refiner.unpackage gl in
-        Refiner.repackage stuff [ g; abstract_proof ] in
-      Tacticals.tclTHENS tacopen [Tacticals.tclSOLVE [Proofview.V82.of_tactic (Tactics.apply proof)]; Proofview.V82.of_tactic (unfold[abstract;abstract_key])] gl
-(* else apply proof gl *)
-  in
-  let introback ist (gens, _) =
-    introstac ~ist
-      (List.map (fun (_,cp) -> match id_of_pattern (interp_cpattern ist gl cp None) with
-        | None -> IPatAnon One
-        | Some id -> IPatId id)
-        (List.tl (List.hd gens))) in
-  Tacticals.tclTHEN (with_dgens gens main ist) (introback ist gens) gl
-
-
 let destProd_or_LetIn sigma c =
   match EConstr.kind sigma c with
   | Prod (n,ty,c) -> RelDecl.LocalAssum (n, ty), c
@@ -321,12 +212,12 @@ let destProd_or_LetIn sigma c =
   | _ -> raise DestKO
 
 let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
-  let mkabs gen = abs_wgen false ist (fun x -> x) gen 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
   | _ -> fun x -> x in
-  let ct = match ct with
+  let ct = match Ssrcommon.ssrterm_of_ast_closure_term ct with
   | (a, (b, Some ct)) ->
     begin match ct.CAst.v with
     | CCast (_, CastConv cty) -> a, (b, Some cty)
@@ -368,11 +259,11 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
          | LetIn(id,b,ty,c) -> EConstr.mkLetIn (id,b,ty,pired c args)
          | _ -> CErrors.anomaly(str"SSR: wlog: pired: " ++ pr_econstr_env env sigma c) in
     c, args, pired c args, pf_merge_uc uc gl in
-  let tacipat pats = introstac ~ist pats in
+  let tacipat pats = introstac pats in
   let tacigens = 
     Tacticals.tclTHEN
-      (Tacticals.tclTHENLIST(List.rev(List.fold_right mkclr gens [cleartac clr0])))
-      (introstac ~ist (List.fold_right mkpats gens [])) in
+      (Tacticals.tclTHENLIST(List.rev(List.fold_right mkclr gens [old_cleartac clr0])))
+      (introstac (List.fold_right mkpats gens [])) in
   let hinttac = hinttac ist true hint in
   let cut_kind, fst_goal_tac, snd_goal_tac =
     match suff, ghave with
@@ -381,13 +272,13 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
     | true, `Gen _ -> assert false
     | false, `Gen id ->
       if gens = [] then errorstrm(str"gen have requires some generalizations");
-      let clear0 = cleartac clr0 in
+      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, _ -> None, Tacticals.tclIDTAC, clear0, pats
       | Some (Some id),_ -> Some id, introid id, clear0, pats
       | Some _,_ ->
-          let id = mk_anon_id "tmp" gl in
+          let id = mk_anon_id "tmp" (Tacmach.pf_ids_of_hyps gl) in
           Some id, introid id, Tacticals.tclTHEN clear0 (Proofview.V82.of_tactic (Tactics.clear [id])), pats in
       let tac_specialize = match id with
       | None -> Tacticals.tclIDTAC
@@ -407,8 +298,8 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
 (** The "suffice" tactic *)
 
 let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) =
-  let htac = Tacticals.tclTHEN (introstac ~ist pats) (hinttac ist true hint) in
-  let c = match c with
+  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)) ->
     begin match ct.CAst.v with
     | CCast (_, CastConv cty) -> a, (b, Some cty)
@@ -423,4 +314,4 @@ let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) =
   let ctac gl =
     let _,ty,_,uc = pf_interp_ty ist gl c in let gl = pf_merge_uc uc gl in
     basecuttac "ssr_suff" ty gl in
-  Tacticals.tclTHENS ctac [htac; Tacticals.tclTHEN (cleartac clr) (introstac ~ist (binders@simpl))]
+  Tacticals.tclTHENS ctac [htac; Tacticals.tclTHEN (old_cleartac clr) (introstac (binders@simpl))]
diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli
index e5b5b58ff..e0a5d3446 100644
--- a/plugins/ssr/ssrfwd.mli
+++ b/plugins/ssr/ssrfwd.mli
@@ -14,24 +14,18 @@ open Ltac_plugin
 
 open Ssrast
 
-val ssrsettac : ist ->  Id.t -> ((ssrfwdfmt * (Ssrmatching_plugin.Ssrmatching.cpattern * ssrterm option)) * ssrdocc) -> v82tac
+val ssrsettac :  Id.t -> ((ssrfwdfmt * (Ssrmatching_plugin.Ssrmatching.cpattern * ast_closure_term option)) * ssrdocc) -> v82tac
 
-val ssrposetac : ist -> (Id.t * (ssrfwdfmt * ssrterm)) -> v82tac
+val ssrposetac : Id.t * (ssrfwdfmt * ast_closure_term) -> v82tac
 
-val havetac :
-           Ssrast.ist ->
+val havetac : ist ->
            bool *
            ((((Ssrast.ssrclear * Ssrast.ssripat list) * Ssrast.ssripats) *
              Ssrast.ssripats) *
-            (((Ssrast.ssrfwdkind * 'a) *
-              ('b * (Glob_term.glob_constr * Constrexpr.constr_expr option))) *
+            (((Ssrast.ssrfwdkind * 'a) * ast_closure_term) *
              (bool * Tacinterp.Value.t option list))) ->
            bool ->
            bool -> v82tac
-val ssrabstract :
-           Tacinterp.interp_sign ->
-           (Ssrast.ssrdocc * Ssrmatching_plugin.Ssrmatching.cpattern) list
-           list * Ssrast.ssrclear -> v82tac
 
 val basecuttac :
            string ->
@@ -46,8 +40,7 @@ val wlogtac :
        option)
     list *
     ('c *
-       (Ssrast.ssrtermkind *
-          (Glob_term.glob_constr * Constrexpr.constr_expr option))) ->
+       ast_closure_term) ->
   Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint ->
   bool ->
   [< `Gen of Names.Id.t option option | `NoGen > `NoGen ] ->
@@ -58,8 +51,7 @@ val sufftac :
   (((Ssrast.ssrhyps * Ssrast.ssripats) * Ssrast.ssripat list) *
      Ssrast.ssripat list) *
     (('a *
-        (Ssrast.ssrtermkind *
-           (Glob_term.glob_constr * Constrexpr.constr_expr option))) *
+        ast_closure_term) *
        (bool * Tacinterp.Value.t option list)) ->
   Tacmach.tactic
 
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index b3be31b7b..1a964bd50 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -6,395 +6,696 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+open Ssrmatching_plugin
 
-open Names
-open Pp
-open Term
-open Tactics
-open Tacticals
-open Tacmach
-open Coqlib
 open Util
-open Evd
-open Printer
+open Names
+
+open Proofview
+open Proofview.Notations
 
-open Ssrmatching_plugin
-open Ssrmatching
 open Ssrast
-open Ssrprinters
-open Ssrcommon
-open Ssrequality
-open Ssrview
-open Ssrelim
-open Ssrbwd
-
-module RelDecl = Context.Rel.Declaration
-(** Extended intro patterns {{{ ***********************************************)
-
-
-(* There are two ways of "applying" a view to term:            *)
-(*  1- using a view hint if the view is an instance of some    *)
-(*     (reflection) inductive predicate.                       *)
-(*  2- applying the view if it coerces to a function, adding   *)
-(*     implicit arguments.                                     *)
-(* They require guessing the view hints and the number of      *)
-(* implicits, respectively, which we do by brute force.        *)
-
-let apply_type x xs = Proofview.V82.of_tactic (apply_type ~typecheck:false x xs)
-
-let new_tac = Proofview.V82.of_tactic
-
-let with_top tac gl =
-  tac_ctx
-    (tclTHENLIST [ introid top_id; tac (EConstr.mkVar top_id); new_tac (clear [top_id])])
-    gl
-
-let tclTHENS_nonstrict tac tacl taclname gl =
-  let tacres = tac gl in
-  let n_gls = List.length (sig_it tacres) in
-  let n_tac = List.length tacl in
-  if n_gls = n_tac then tclTHENS_a (fun _ -> tacres) tacl gl else
-  if n_gls = 0 then tacres else
-  let pr_only n1 n2 = if n1 < n2 then str "only " else mt () in
-  let pr_nb n1 n2 name =
-    pr_only n1 n2 ++ int n1 ++ str (" " ^ String.plural n1 name) in
-  errorstrm (pr_nb n_tac n_gls taclname ++ spc ()
-             ++ str "for " ++ pr_nb n_gls n_tac "subgoal")
-
-let rec nat_of_n n =
-  if n = 0 then EConstr.mkConstruct path_of_O
-  else EConstr.mkApp (EConstr.mkConstruct path_of_S, [|nat_of_n (n-1)|])
-
-let ssr_abstract_id = Summary.ref ~name:"SSR:abstractid" 0
-
-let mk_abstract_id () = incr ssr_abstract_id; nat_of_n !ssr_abstract_id
-
-let ssrmkabs id gl =
-  let env, concl = pf_env gl, Tacmach.pf_concl gl in
+
+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
+
+end = struct (* {{{ *)
+
+module State : sig
+
+  (* to_clear API *)
+  val isCLR_PUSH    : Id.t -> unit tactic
+  val isCLR_PUSHL   : Id.t list -> unit tactic
+  val isCLR_CONSUME : unit tactic
+
+  (* Some data may expire *)
+  val isTICK : ssripat -> unit tactic
+
+  val isPRINT : Proofview.Goal.t -> Pp.t
+
+end = struct (* {{{ *)
+
+type istate = {
+
+  (* Delayed clear *)
+  to_clear : Id.t list;
+
+}
+
+let empty_state = {
+  to_clear = [];
+}
+
+include Ssrcommon.MakeState(struct
+  type state = istate
+  let init = empty_state
+end)
+
+let isPRINT g =
+  let state = get g in
+  Pp.(str"{{ to_clear: " ++
+        prlist_with_sep spc Id.print state.to_clear ++ spc () ++
+      str" }}")
+
+
+let isCLR_PUSH id =
+  tclGET (fun { to_clear = ids } ->
+  tclSET { to_clear = id :: ids })
+
+let isCLR_PUSHL more_ids =
+  tclGET (fun { to_clear = ids } ->
+  tclSET { to_clear = more_ids @ ids })
+
+let isCLR_CONSUME =
+  tclGET (fun { to_clear = ids } ->
+  tclSET { to_clear = [] } <*>
+  Tactics.clear ids)
+
+
+let isTICK _ = tclUNIT ()
+
+end (* }}} *************************************************************** *)
+
+open State
+
+(** [=> *] ****************************************************************)
+(** [nb_assums] returns the number of dependent premises *)
+(** Warning: unlike [nb_deps_assums], it does not perform reduction *)
+let rec nb_assums cur env sigma t =
+  match EConstr.kind sigma t with
+  | Term.Prod(name,ty,body) ->
+     nb_assums (cur+1) env sigma body
+  | Term.LetIn(name,ty,t1,t2) ->
+    nb_assums (cur+1) env sigma t2
+  | Term.Cast(t,_,_) ->
+     nb_assums cur env sigma t
+  | _ -> cur
+let nb_assums = nb_assums 0
+
+let intro_anon_all = Goal.enter begin fun gl ->
+  let env = Goal.env gl in
+  let sigma = Goal.sigma gl in
+  let g = Goal.concl gl in
+  let n = nb_assums env sigma g in
+  Tacticals.New.tclDO n Ssrcommon.tclINTRO_ANON
+end
+
+(** [intro_drop] behaves like [intro_anon] but registers the id of the
+    introduced assumption for a delayed clear. *)
+let intro_drop =
+  Ssrcommon.tclINTRO ~id:None
+    ~conclusion:(fun ~orig_name:_ ~new_name -> isCLR_PUSH new_name)
+
+(** [intro_end] performs the actions that have been delayed. *)
+let intro_end =
+  Ssrcommon.tcl0G (isCLR_CONSUME)
+
+(** [=> _] *****************************************************************)
+let intro_clear ids future_ipats =
+  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
+    in
+    Tactics.rename_hyp ren <*>
+    isCLR_PUSHL clear_ids
+end
+
+(** [=> []] *****************************************************************)
+let tac_case t =
+  Goal.enter begin fun _ ->
+    Ssrcommon.tacTYPEOF t >>= fun ty ->
+    Ssrcommon.tacIS_INJECTION_CASE ~ty t >>= fun is_inj ->
+    if is_inj then
+      V82.tactic ~nf_evars:false (Ssrelim.perform_injection t)
+    else
+      Ssrelim.ssrscasetac t
+end
+
+(** [=> [: id]] ************************************************************)
+let mk_abstract_id =
+  let open Coqlib in
+  let ssr_abstract_id = Summary.ref ~name:"SSR:abstractid" 0 in
+begin fun () ->
+  let rec nat_of_n n =
+    if n = 0 then EConstr.mkConstruct path_of_O
+    else EConstr.mkApp (EConstr.mkConstruct path_of_S, [|nat_of_n (n-1)|]) in
+  incr ssr_abstract_id; nat_of_n !ssr_abstract_id
+end
+
+let tcltclMK_ABSTRACT_VAR id = Goal.enter begin fun gl ->
+  let env, concl = Goal.(env gl, concl gl) in
   let step = begin fun sigma ->
     let (sigma, (abstract_proof, abstract_ty)) =
       let (sigma, (ty, _)) =
         Evarutil.new_type_evar env sigma Evd.univ_flexible_alg in
-      let (sigma, ablock) = mkSsrConst "abstract_lock" env sigma in
+      let (sigma, ablock) = Ssrcommon.mkSsrConst "abstract_lock" env sigma in
       let (sigma, lock) = Evarutil.new_evar env sigma ablock in
-      let (sigma, abstract) = mkSsrConst "abstract" env sigma in
-      let abstract_ty = EConstr.mkApp(abstract, [|ty;mk_abstract_id ();lock|]) in
-      let (sigma, m) = Evarutil.new_evar env sigma abstract_ty in
-      (sigma, (m, abstract_ty)) in
+      let (sigma, abstract) = Ssrcommon.mkSsrConst "abstract" env sigma in
+      let abstract_ty =
+        EConstr.mkApp(abstract, [|ty;mk_abstract_id ();lock|]) in
+      let sigma, m = Evarutil.new_evar env sigma abstract_ty in
+      sigma, (m, abstract_ty) in
     let sigma, kont =
-      let rd = RelDecl.LocalAssum (Name id, abstract_ty) in
-      let (sigma, ev) = Evarutil.new_evar (EConstr.push_rel rd env) sigma concl in
-      (sigma, ev)
+      let rd = Context.Rel.Declaration.LocalAssum (Name id, abstract_ty) in
+      let sigma, ev = Evarutil.new_evar (EConstr.push_rel rd env) sigma concl in
+      sigma, ev
     in
-(*    pp(lazy(pr_econstr concl)); *)
-    let term = EConstr.(mkApp (mkLambda(Name id,abstract_ty,kont) ,[|abstract_proof|])) in
+    let term =
+      EConstr.(mkApp (mkLambda(Name id,abstract_ty,kont),[|abstract_proof|])) in
     let sigma, _ = Typing.type_of env sigma term in
-    (sigma, term)
+    sigma, term
   end in
-  Proofview.V82.of_tactic
-    (Proofview.tclTHEN
-      (Tactics.New.refine ~typecheck:false step)
-      (Proofview.tclFOCUS 1 3 Proofview.shelve)) gl
-
-let ssrmkabstac ids =
-  List.fold_right (fun id tac -> tclTHENFIRST (ssrmkabs id) tac) ids tclIDTAC
-
-(* introstac: for "move" and "clear", tclEQINTROS: for "case" and "elim" *)
-(* This block hides the spaghetti-code needed to implement the only two  *)
-(* tactics that should be used to process intro patters.                 *)
-(* The difficulty is that we don't want to always rename, but we can     *)
-(* compute needeed renamings only at runtime, so we theread a tree like  *)
-(* imperativestructure so that outer renamigs are inherited by inner     *)
-(* ipts and that the cler performed at the end of ipatstac clears hyps   *)
-(* eventually renamed at runtime.                                        *)
-let delayed_clear force rest clr gl = 
-  let gl, ctx = pull_ctx gl in
-  let hyps = pf_hyps gl in
-  let () = if not force then List.iter (check_hyp_exists hyps) clr in
-  if List.exists (fun x -> force || is_name_in_ipats (hyp_id x) rest) clr then
-    let ren_clr, ren = 
-      List.split (List.map (fun x ->
-        let x = hyp_id x in
-        let x' = mk_anon_id (Id.to_string x) gl in
-        x', (x, x')) clr) in
-    let ctx = { ctx with delayed_clears = ren_clr @ ctx.delayed_clears } in
-    let gl = push_ctx ctx gl in
-    tac_ctx (Proofview.V82.of_tactic (rename_hyp ren)) gl 
-  else
-    let ctx = { ctx with delayed_clears = hyps_ids clr @ ctx.delayed_clears } in
-    let gl = push_ctx ctx gl in
-    tac_ctx tclIDTAC gl
-      
-(* Common code to handle generalization lists along with the defective case *)
+  Tactics.New.refine ~typecheck:false step <*>
+  tclFOCUS 1 3 Proofview.shelve
+end
+
+let tclMK_ABSTRACT_VARS ids =
+  List.fold_right (fun id tac ->
+    Tacticals.New.tclTHENFIRST (tcltclMK_ABSTRACT_VAR id) tac) ids (tclUNIT ())
+
+(* Debugging *)
+let tclLOG p t =
+  tclUNIT () >>= begin fun () ->
+    Ssrprinters.ppdebug (lazy Pp.(str "exec: " ++ Ssrprinters.pr_ipat p));
+    tclUNIT ()
+  end <*>
+  Goal.enter begin fun g ->
+    Ssrprinters.ppdebug (lazy Pp.(str" on state:" ++ spc () ++
+      isPRINT g ++
+      str" goal:" ++ spc () ++ Printer.pr_goal (Goal.print g)));
+    tclUNIT ()
+  end
+  <*>
+    t p
+  <*>
+  Goal.enter begin fun g ->
+    Ssrprinters.ppdebug (lazy Pp.(str "done: " ++ isPRINT g));
+    tclUNIT ()
+  end
+
+let rec ipat_tac1 future_ipats ipat : unit tactic =
+  match ipat with
+  | IPatView l ->
+      Ssrview.tclIPAT_VIEWS ~views:l
+        ~conclusion:(fun ~to_clear:clr -> intro_clear clr future_ipats)
+  | IPatDispatch ipatss ->
+      tclEXTEND (List.map ipat_tac ipatss) (tclUNIT ()) []
+
+  | IPatId id -> Ssrcommon.tclINTRO_ID id
+
+  | IPatCase ipatss ->
+     tclIORPAT (Ssrcommon.tclWITHTOP tac_case) ipatss
+  | IPatInj ipatss ->
+     tclIORPAT (Ssrcommon.tclWITHTOP
+       (fun t -> V82.tactic  ~nf_evars:false (Ssrelim.perform_injection t))) ipatss
+
+  | IPatAnon Drop -> intro_drop
+  | IPatAnon One -> Ssrcommon.tclINTRO_ANON
+  | IPatAnon All -> intro_anon_all
+
+  | IPatNoop -> tclUNIT ()
+  | IPatSimpl Nop -> tclUNIT ()
+
+  | IPatClear ids -> intro_clear (List.map Ssrcommon.hyp_id ids) future_ipats
+
+  | IPatSimpl (Simpl n) ->
+       V82.tactic ~nf_evars:false (Ssrequality.simpltac (Simpl n))
+  | IPatSimpl (Cut n) ->
+       V82.tactic ~nf_evars:false (Ssrequality.simpltac (Cut n))
+  | IPatSimpl (SimplCut (n,m)) ->
+       V82.tactic ~nf_evars:false (Ssrequality.simpltac (SimplCut (n,m)))
+
+  | IPatRewrite (occ,dir) ->
+     Ssrcommon.tclWITHTOP
+       (fun x -> V82.tactic  ~nf_evars:false (Ssrequality.ipat_rewrite occ dir x))
+
+  | IPatAbstractVars ids -> tclMK_ABSTRACT_VARS ids
+
+  | IPatTac t -> t
+
+and ipat_tac pl : unit tactic =
+  match pl with
+  | [] -> tclUNIT ()
+  | pat :: pl ->
+      Ssrcommon.tcl0G (tclLOG pat (ipat_tac1 pl)) <*>
+      isTICK pat <*>
+      ipat_tac pl
+
+and tclIORPAT tac = function
+  | [[]] -> tac
+  | p -> Tacticals.New.tclTHENS tac (List.map ipat_tac p)
 
-let with_defective maintac deps clr ist gl =
-  let top_id =
-    match EConstr.kind_of_type (project gl) (pf_concl gl) with
-    | ProdType (Name id, _, _)
-      when has_discharged_tag (Id.to_string id) -> id
-    | _ -> top_id in
-  let top_gen = mkclr clr, cpattern_of_id top_id in
-  tclTHEN (introid top_id) (maintac deps top_gen ist) gl
-
-let with_defective_a maintac deps clr ist gl =
-  let sigma = sig_sig gl in
-  let top_id =
-    match EConstr.kind_of_type sigma (without_ctx pf_concl gl) with
-    | ProdType (Name id, _, _)
-      when has_discharged_tag (Id.to_string id) -> id
-    | _ -> top_id in
-  let top_gen = mkclr clr, cpattern_of_id top_id in
-  tclTHEN_a (tac_ctx (introid top_id)) (maintac deps top_gen ist) gl
-
-let with_dgens (gensl, clr) maintac ist = match gensl with
-  | [deps; []] -> with_defective maintac deps clr ist
-  | [deps; gen :: gens] ->
-    tclTHEN (genstac (gens, clr) ist) (maintac deps gen ist)
-  | [gen :: gens] -> tclTHEN (genstac (gens, clr) ist) (maintac [] gen ist)
-  | _ -> with_defective maintac [] clr ist
-
-let viewmovetac_aux ?(next=ref []) clear name_ref (_, vl as v) _ gen ist gl =
-  let cl, c, clr, gl, gen_pat =
-    let gl, ctx = pull_ctx gl in
-    let _, gen_pat, a, b, c, ucst, gl = pf_interp_gen_aux ist gl false gen in
-    a, b ,c, push_ctx ctx (pf_merge_uc ucst gl), gen_pat in
-  let clr = if clear then clr else [] in
-  name_ref := (match id_of_pattern gen_pat with Some id -> id | _ -> top_id);
-  let clr = if clear then clr else [] in
-  if vl = [] then tac_ctx (genclrtac cl [c] clr) gl
-  else
-    let _, _, gl =
-      pfa_with_view ist ~next v cl c
-        (fun cl c -> tac_ctx (genclrtac cl [c] clr)) clr gl in
-      gl
+let split_at_first_case ipats =
+  let rec loop acc = function
+    | (IPatSimpl _ | IPatClear _) as x :: rest -> loop (x :: acc) rest
+    | IPatCase _ as x :: xs -> CList.rev acc, Some x, xs
+    | pats -> CList.rev acc, None, pats
+  in
+    loop [] ipats
 
-let move_top_with_view ~next c r v =
-  with_defective_a (viewmovetac_aux ~next c r v) [] []
+let ssr_exception is_on = function
+  | Some (IPatCase l) when is_on -> Some (IPatDispatch l)
+  | x -> x
 
-type block_names = (int * EConstr.types array) option
+let option_to_list = function None -> [] | Some x -> [x]
 
-let (introstac : ?ist:Tacinterp.interp_sign -> ssripats -> Tacmach.tactic),
-    (tclEQINTROS : ?ind:block_names ref -> ?ist:Tacinterp.interp_sign ->
-                     Tacmach.tactic -> Tacmach.tactic -> ssripats ->
-                      Tacmach.tactic)
-=
+let main ?eqtac ~first_case_is_dispatch ipats =
+  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)
 
-  let rec ipattac ?ist ~next p : tac_ctx tac_a = fun gl ->
-(*     pp(lazy(str"ipattac: " ++ pr_ipat p)); *)
-    match p with
-    | IPatAnon Drop ->
-        let id, gl = with_ctx new_wild_id gl in
-        tac_ctx (introid id) gl
-    | IPatAnon All -> tac_ctx intro_all gl
-    (* TODO
-    | IPatAnon Temporary ->
-        let (id, orig), gl = with_ctx new_tmp_id gl in
-        introid_a ~orig id gl
-                     *)
-    | IPatCase(iorpat) ->
-        tclIORPAT ?ist (with_top (ssrscasetac false)) iorpat gl
-    | IPatInj iorpat ->
-        tclIORPAT ?ist (with_top (ssrscasetac true)) iorpat gl
-    | IPatRewrite (occ, dir) ->
-        with_top (ipat_rewrite occ dir) gl
-    | IPatId id -> tac_ctx (introid id) gl
-    | IPatNewHidden idl -> tac_ctx (ssrmkabstac idl) gl
-    | IPatSimpl sim ->
-        tac_ctx (simpltac sim) gl
-    | IPatClear clr ->
-        delayed_clear false !next clr gl
-    | IPatAnon One -> tac_ctx intro_anon gl
-    | IPatNoop -> tac_ctx tclIDTAC gl
-    | IPatView v ->
-        let ist =
-          match ist with Some x -> x | _ -> anomaly "ipat: view with no ist" in
-        let next_keeps =
-          match !next with (IPatCase _ | IPatRewrite _)::_ -> false | _ -> true in
-        let top_id = ref top_id in
-        tclTHENLIST_a [
-          (move_top_with_view ~next next_keeps top_id (next_keeps,v) ist);
-          (fun gl ->
-             let hyps = without_ctx pf_hyps gl in
-             if not next_keeps && test_hypname_exists hyps !top_id then
-               delayed_clear true !next [SsrHyp (Loc.tag !top_id)] gl
-             else tac_ctx tclIDTAC gl)]
-        gl
-
-  and tclIORPAT ?ist tac = function
-  | [[]] -> tac
-  | orp -> tclTHENS_nonstrict tac (List.map (ipatstac ?ist) orp) "intro pattern"
-
-  and ipatstac ?ist ipats gl =
-    let rec aux ipats gl =
-      match ipats with
-      | [] -> tac_ctx tclIDTAC gl
-      | p :: ps ->
-          let next = ref ps in
-          let gl = ipattac ?ist ~next p gl in
-          tac_on_all gl (aux !next)
-    in
-      aux ipats gl
-  in
+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
+
+let tclIPATssr ip =
+  Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip));
+  IpatMachine.main ~first_case_is_dispatch:true ip
 
-  let rec split_itacs ?ist ~ind tac' = function
-    | (IPatSimpl _ | IPatClear _ as spat) :: ipats' ->
-        let tac = ipattac ?ist ~next:(ref ipats') spat in
-        split_itacs ?ist ~ind (tclTHEN_a tac' tac) ipats'
-    | IPatCase iorpat :: ipats' -> 
-        tclIORPAT ?ist tac' iorpat, ipats'
-    | ipats' -> tac', ipats' in
-
-  let combine_tacs tac eqtac ipats ?ist ~ind gl =
-    let tac1, ipats' = split_itacs ?ist ~ind tac ipats in
-    let tac2 = ipatstac ?ist ipats' in
-    tclTHENLIST_a [ tac1; eqtac; tac2 ] gl in
- 
-  (* Exported code *) 
-  let introstac ?ist ipats gl =
-    with_fresh_ctx (tclTHENLIST_a [
-      ipatstac ?ist ipats;
-      gen_tmp_ids ?ist;
-      clear_wilds_and_tmp_and_delayed_ids
-    ]) gl in
-  
-  let tclEQINTROS ?(ind=ref None) ?ist tac eqtac ipats gl =
-    with_fresh_ctx (tclTHENLIST_a [
-      combine_tacs (tac_ctx tac) (tac_ctx eqtac) ipats ?ist ~ind;
-      gen_tmp_ids ?ist;
-      clear_wilds_and_tmp_and_delayed_ids;
-    ]) gl in
-
-  introstac, tclEQINTROS
-;;
-
-(* Intro patterns processing for elim tactic*)
-let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr gl =
-  (* Utils of local interest only *)
-  let iD s ?t gl = let t = match t with None -> pf_concl gl | Some x -> x in
-                   ppdebug(lazy Pp.(str s ++ pr_econstr_env (pf_env gl) (project gl) t)); Tacticals.tclIDTAC gl in
-  let protectC, gl = pf_mkSsrConst "protect_term" gl in
-  let eq, gl = pf_fresh_global (Coqlib.build_coq_eq ()) gl in
-  let eq = EConstr.of_constr eq in
-  let fire_subst gl t = Reductionops.nf_evar (project gl) t in
-  let intro_eq = 
-    match eqid with 
-    | Some (IPatId ipat) when not is_rec -> 
-       let rec intro_eq gl = match EConstr.kind_of_type (project gl) (pf_concl gl) with
-         | ProdType (_, src, tgt) -> 
-            (match EConstr.kind_of_type (project gl) src with
-             | AtomicType (hd, _) when EConstr.eq_constr (project gl) hd protectC -> 
-                Tacticals.tclTHENLIST [unprotecttac; introid ipat] gl
-             | _ -> Tacticals.tclTHENLIST [ iD "IA"; Ssrcommon.intro_anon; intro_eq] gl)
-         |_ -> errorstrm (Pp.str "Too many names in intro pattern") in
-       intro_eq
-    | Some (IPatId ipat) -> 
-       let name gl = mk_anon_id "K" gl in
-       let intro_lhs gl = 
+(* Common code to handle generalization lists along with the defective case *)
+let with_defective maintac deps clr = Goal.enter begin fun g ->
+  let sigma, concl = Goal.(sigma g, concl g) in
+  let top_id =
+    match EConstr.kind_of_type sigma concl with
+    | Term.ProdType (Name id, _, _)
+      when Ssrcommon.is_discharged_id id -> id
+    | _ -> Ssrcommon.top_id in
+  let top_gen = Ssrequality.mkclr clr, Ssrmatching.cpattern_of_id top_id in
+  Ssrcommon.tclINTRO_ID top_id <*> maintac deps top_gen
+end
+
+let with_dgens { dgens; gens; clr } maintac = match gens with
+  | [] -> with_defective maintac dgens clr
+  | gen :: gens ->
+      V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, clr)) <*> maintac dgens gen
+
+let mkCoqEq env sigma =
+  let eq = Coqlib.((build_coq_eq_data ()).eq) in
+  let sigma, eq = EConstr.fresh_global env sigma eq in
+  eq, sigma
+
+let mkCoqRefl t c env sigma =
+  let refl = Coqlib.((build_coq_eq_data()).refl) in
+  let sigma, refl = EConstr.fresh_global env sigma refl in
+  EConstr.mkApp (refl, [|t; c|]), sigma
+
+(** Intro patterns processing for elim tactic, in particular when used in
+    conjunction with equation generation as in [elim E: x] *)
+let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr =
+  let intro_eq =
+    match eqid with
+    | 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
+         | Term.ProdType (_, src, tgt) -> begin
+             match EConstr.kind_of_type sigma src with
+             | Term.AtomicType (hd, _) when Ssrcommon.is_protect hd env sigma ->
+                V82.tactic ~nf_evars:false Ssrcommon.unprotecttac <*>
+                Ssrcommon.tclINTRO_ID ipat
+             | _ -> Ssrcommon.tclINTRO_ANON <*> intro_eq ()
+             end
+         |_ -> Ssrcommon.errorstrm (Pp.str "Too many names in intro pattern")
+       end in
+       intro_eq ()
+    | Some (IPatId ipat) ->
+       let intro_lhs = Goal.enter begin fun g ->
+         let sigma = Goal.sigma g in
          let elim_name = match clr, what with
            | [SsrHyp(_, x)], _ -> x
-           | _, `EConstr(_,_,t) when EConstr.isVar (project gl) t -> EConstr.destVar (project gl) t
-           | _ -> name gl in
-         if is_name_in_ipats elim_name ipats then introid (name gl) gl
-         else introid elim_name gl
-       in
-       let rec gen_eq_tac gl =
-         let concl = pf_concl gl in
-         let ctx, last = EConstr.decompose_prod_assum (project gl) concl in
-         let args = match EConstr.kind_of_type (project gl) last with
-           | AtomicType (hd, args) -> assert(EConstr.eq_constr (project gl) hd protectC); args
+           | _, `EConstr(_,_,t) when EConstr.isVar sigma t ->
+              EConstr.destVar sigma t
+           | _ -> Ssrcommon.mk_anon_id "K" (Tacmach.New.pf_ids_of_hyps g) in
+         let elim_name =
+           if Ssrcommon.is_name_in_ipats elim_name ipats then
+             Ssrcommon.mk_anon_id "K" (Tacmach.New.pf_ids_of_hyps g)
+           else elim_name
+         in
+         Ssrcommon.tclINTRO_ID elim_name
+       end in
+       let rec gen_eq_tac () = Goal.enter begin fun g ->
+         let sigma, env, concl = Goal.(sigma g, env g, concl g) in
+         let sigma, eq =
+           EConstr.fresh_global env sigma (Coqlib.build_coq_eq ()) in
+         let ctx, last = EConstr.decompose_prod_assum sigma concl in
+         let args = match EConstr.kind_of_type sigma last with
+           | Term.AtomicType (hd, args) ->
+               assert(Ssrcommon.is_protect hd env sigma);
+               args
            | _ -> assert false in
          let case = args.(Array.length args-1) in
-         if not(EConstr.Vars.closed0 (project gl) case) then Tacticals.tclTHEN Ssrcommon.intro_anon gen_eq_tac gl
+         if not(EConstr.Vars.closed0 sigma case)
+         then Ssrcommon.tclINTRO_ANON <*> gen_eq_tac ()
          else
-           let gl, case_ty = pfe_type_of gl case in 
-           let refl = EConstr.mkApp (eq, [|EConstr.Vars.lift 1 case_ty; EConstr.mkRel 1; EConstr.Vars.lift 1 case|]) in
-           let new_concl = fire_subst gl
-                                      EConstr.(mkProd (Name (name gl), case_ty, mkArrow refl (Vars.lift 2 concl))) in 
-           let erefl, gl = mkRefl case_ty case gl in
-           let erefl = fire_subst gl erefl in
-           apply_type new_concl [case;erefl] gl in
-       Tacticals.tclTHENLIST [gen_eq_tac; intro_lhs; introid ipat]
-    | _ -> Tacticals.tclIDTAC in
-  let unprot = if eqid <> None && is_rec then unprotecttac else Tacticals.tclIDTAC in
-  tclEQINTROS ?ist ssrelim (Tacticals.tclTHENLIST [intro_eq; unprot]) ipats gl
-
-(* General case *)
-let tclINTROS ist t ip = tclEQINTROS ~ist (t ist) tclIDTAC ip
-
-(* }}} *)
-
-let viewmovetac ?next v deps gen ist gl = 
- with_fresh_ctx
-   (tclTHEN_a
-     (viewmovetac_aux ?next true (ref top_id) v deps gen ist)
-      clear_wilds_and_tmp_and_delayed_ids)
-     gl
-
-let mkCoqEq gl =
-  let sigma = project gl in
-  let (sigma, eq) = EConstr.fresh_global (pf_env gl) sigma (build_coq_eq_data()).eq in
-  let gl = { gl with sigma } in
-  eq, gl
-
-let mkEq dir cl c t n gl =
-  let open EConstr in
-  let eqargs = [|t; c; c|] in eqargs.(dir_org dir) <- mkRel n;
-  let eq, gl = mkCoqEq gl in
-  let refl, gl = mkRefl t c gl in
-  mkArrow (mkApp (eq, eqargs)) (EConstr.Vars.lift 1 cl), refl, gl
-
-let pushmoveeqtac cl c gl =
+           Ssrcommon.tacTYPEOF case >>= fun case_ty ->
+           let open EConstr in
+           let refl =
+             mkApp (eq, [|Vars.lift 1 case_ty; mkRel 1; Vars.lift 1 case|]) in
+           let name = Ssrcommon.mk_anon_id "K" (Tacmach.New.pf_ids_of_hyps g) in
+
+           let new_concl =
+             mkProd (Name name, case_ty, mkArrow refl (Vars.lift 2 concl)) in
+           let erefl, sigma = mkCoqRefl case_ty case env sigma in
+           Proofview.Unsafe.tclEVARS sigma <*>
+           Tactics.apply_type ~typecheck:true new_concl [case;erefl]
+       end in
+       gen_eq_tac () <*>
+       intro_lhs <*>
+       Ssrcommon.tclINTRO_ID ipat
+    | _ -> tclUNIT () in
+  let unprot =
+    if eqid <> None && is_rec
+    then V82.tactic ~nf_evars:false Ssrcommon.unprotecttac else tclUNIT () in
+  V82.of_tactic begin
+    V82.tactic ~nf_evars:false ssrelim <*>
+    tclIPAT_EQ (intro_eq <*> unprot) ipats
+  end
+
+let mkEq dir cl c t n env sigma =
   let open EConstr in
-  let x, t, cl1 = destProd (project gl) cl in
-  let cl2, eqc, gl = mkEq R2L cl1 c t 1 gl in
-  apply_type (mkProd (x, t, cl2)) [c; eqc] gl
-
-let eqmovetac _ gen ist gl =
-  let cl, c, _, gl = pf_interp_gen ist gl false gen in pushmoveeqtac cl c gl
-
-let movehnftac gl = match EConstr.kind (project gl) (pf_concl gl) with
-  | Prod _ | LetIn _ -> tclIDTAC gl
-  | _ -> new_tac hnf_in_concl gl
+  let eqargs = [|t; c; c|] in
+  eqargs.(Ssrequality.dir_org dir) <- mkRel n;
+  let eq, sigma = mkCoqEq env sigma in
+  let refl, sigma = mkCoqRefl t c env sigma in
+  mkArrow (mkApp (eq, eqargs)) (Vars.lift 1 cl), refl, sigma
+
+(** in [tac/v: last gens..] the first (last to be run) generalization is
+    "special" in that is it also the main argument of [tac] and is eventually
+    to be processed forward with view [v]. The behavior implemented is
+    very close to [tac: (v last) gens..] but:
+    - [v last] may use a view adaptor
+    - eventually clear for [last] is taken into account
+    - [tac/v {clr}] is also supported, and [{clr}] is to be run later
+    The code here does not "grab" [v last] nor apply [v] to [last], see the
+    [tacVIEW_THEN_GRAB] combinator. *)
+let tclLAST_GEN ~to_ind ((oclr, occ), t) conclusion = tclINDEPENDENTL begin
+  Ssrcommon.tacSIGMA >>= fun sigma0 ->
+  Goal.enter_one begin fun g ->
+  let pat = Ssrmatching.interp_cpattern sigma0 t None in
+  let cl0, env, sigma, hyps = Goal.(concl g, env g, sigma g, hyps g) in
+  let cl = EConstr.to_constr sigma cl0 in
+  let (c, ucst), cl =
+    try Ssrmatching.fill_occ_pattern ~raise_NoMatch:true env sigma cl pat occ 1
+    with Ssrmatching.NoMatch -> Ssrmatching.redex_of_pattern env pat, cl in
+  let sigma = Evd.merge_universe_context sigma ucst in
+  let c, cl = EConstr.of_constr c, EConstr.of_constr cl in
+  let clr =
+    Ssrcommon.interp_clr sigma (oclr, (Ssrmatching.tag_of_cpattern t,c)) in
+  (* Historically in Coq, and hence in ssr, [case t] accepts [t] of type
+     [A.. -> Ind] and opens new goals for [A..] as well as for the branches
+     of [Ind], see the [~to_ind] argument *)
+  if not(Termops.occur_existential sigma c) then
+    if Ssrmatching.tag_of_cpattern t = Ssrprinters.xWithAt then
+      if not (EConstr.isVar sigma c) then
+        Ssrcommon.errorstrm Pp.(str "@ can be used with variables only")
+      else match Context.Named.lookup (EConstr.destVar sigma c) hyps with
+      | Context.Named.Declaration.LocalAssum _ ->
+          Ssrcommon.errorstrm Pp.(str "@ can be used with let-ins only")
+      | Context.Named.Declaration.LocalDef (name, b, ty) ->
+          Unsafe.tclEVARS sigma <*>
+          tclUNIT (true, EConstr.mkLetIn (Name name,b,ty,cl), c, clr)
+    else
+      Unsafe.tclEVARS sigma <*>
+      Ssrcommon.tacMKPROD c cl >>= fun ccl ->
+      tclUNIT (false, ccl, c, clr)
+  else
+    if to_ind && occ = None then
+      let _, p, _, ucst' =
+        (* TODO: use abs_evars2 *)
+        Ssrcommon.pf_abs_evars sigma0 (fst pat, c) in
+      let sigma = Evd.merge_universe_context sigma ucst' in
+      Unsafe.tclEVARS sigma <*>
+      Ssrcommon.tacTYPEOF p >>= fun pty ->
+      (* TODO: check bug: cl0 no lift? *)
+      let ccl = EConstr.mkProd (Ssrcommon.constr_name sigma c, pty, cl0) in
+      tclUNIT (false, ccl, p, clr)
+  else
+    Ssrcommon.errorstrm Pp.(str "generalized term didn't match")
+end end >>= begin
+  fun infos -> tclDISPATCH (infos |> List.map conclusion)
+end
+
+(** a typical mate of [tclLAST_GEN] doing the job of applying the views [cs]
+    to [c] and generalizing the resulting term *)
+let tacVIEW_THEN_GRAB ?(simple_types=true)
+  vs ~conclusion (is_letin, new_concl, c, clear)
+=
+  Ssrview.tclWITH_FWD_VIEWS ~simple_types ~subject:c ~views:vs
+  ~conclusion:(fun t ->
+    Ssrcommon.tacCONSTR_NAME c >>= fun name ->
+    Goal.enter_one ~__LOC__ begin fun g ->
+      let sigma, env = Goal.sigma g, Goal.env g in
+      Ssrcommon.tacMKPROD t ~name
+        (Termops.subst_term sigma t (* NOTE: we grab t here *)
+          (Termops.prod_applist sigma new_concl [c])) >>=
+      conclusion is_letin t clear
+    end)
+
+(* Elim views are elimination lemmas, so the eliminated term is not added *)
+(* to the dependent terms as for "case", unless it actually occurs in the  *)
+(* goal, the "all occurrences" {+} switch is used, or the equation switch  *)
+(* is used and there are no dependents.                                    *)
+
+let ssrelimtac (view, (eqid, (dgens, ipats))) =
+  let ndefectelimtac view eqid ipats deps gen =
+    match view with
+    | [v] ->
+      Ssrcommon.tclINTERP_AST_CLOSURE_TERM_AS_CONSTR v >>= fun cs ->
+      tclDISPATCH (List.map (fun elim ->
+        V82.tactic ~nf_evars:false
+          (Ssrelim.ssrelim deps (`EGen gen) ~elim eqid (elim_intro_tac ipats)))
+        cs)
+    | [] ->
+      tclINDEPENDENT
+        (V82.tactic ~nf_evars:false
+          (Ssrelim.ssrelim deps (`EGen gen) eqid (elim_intro_tac ipats)))
+    | _ ->
+      Ssrcommon.errorstrm
+        Pp.(str "elim: only one elimination lemma can be provided")
+  in
+  with_dgens dgens (ndefectelimtac view eqid ipats)
+
+let ssrcasetac (view, (eqid, (dgens, ipats))) =
+  let ndefectcasetac view eqid ipats deps ((_, occ), _ as gen) =
+    tclLAST_GEN ~to_ind:true gen (fun (_, cl, c, clear as info) ->
+      let conclusion _ vc _clear _cl =
+        Ssrcommon.tacIS_INJECTION_CASE vc >>= fun inj ->
+        let simple = (eqid = None && deps = [] && occ = None) in
+        if simple && inj then
+          V82.tactic ~nf_evars:false (Ssrelim.perform_injection vc) <*>
+          Tactics.clear (List.map Ssrcommon.hyp_id clear) <*>
+          tclIPATssr ipats
+        else
+        (* macro for "case/v E: x" ---> "case E: x / (v x)" *)
+          let deps, clear, occ =
+            if view <> [] && eqid <> None && deps = []
+            then [gen], [], None
+            else deps, clear, occ in
+          V82.tactic ~nf_evars:false
+            (Ssrelim.ssrelim ~is_case:true deps (`EConstr (clear, occ, vc))
+              eqid (elim_intro_tac ipats))
+      in
+      if view = [] then conclusion false c clear c
+      else tacVIEW_THEN_GRAB ~simple_types:false view ~conclusion info)
+  in
+  with_dgens dgens (ndefectcasetac view eqid ipats)
+
+let ssrscasetoptac = Ssrcommon.tclWITHTOP Ssrelim.ssrscase_or_inj_tac
+let ssrselimtoptac = Ssrcommon.tclWITHTOP Ssrelim.elimtac
+
+(** [move] **************************************************************)
+let pushmoveeqtac cl c = Goal.enter begin fun g ->
+  let env, sigma = Goal.(env g, sigma g) in
+  let x, t, cl1 = EConstr.destProd sigma cl in
+  let cl2, eqc, sigma = mkEq R2L cl1 c t 1 env sigma in
+  Unsafe.tclEVARS sigma <*>
+  Tactics.apply_type ~typecheck:true (EConstr.mkProd (x, t, cl2)) [c; eqc]
+end
+
+let eqmovetac _ gen = Goal.enter begin fun g ->
+  Ssrcommon.tacSIGMA >>= fun gl ->
+  let cl, c, _, gl = Ssrcommon.pf_interp_gen gl false gen in
+  Unsafe.tclEVARS (Tacmach.project gl) <*>
+  pushmoveeqtac cl c
+end
 
 let rec eqmoveipats eqpat = function
-  | (IPatSimpl _ | IPatClear _ as ipat) :: ipats -> ipat :: eqmoveipats eqpat ipats
-  | (IPatAnon All :: _ | []) as ipats -> IPatAnon One :: eqpat :: ipats
-   | ipat :: ipats -> ipat :: eqpat :: ipats
-
-let ssrmovetac ist = function
-  | _::_ as view, (_, (dgens, ipats)) ->
-    let next = ref ipats in
-    let dgentac = with_dgens dgens (viewmovetac ~next (true, view)) ist in
-    tclTHEN dgentac (fun gl -> introstac ~ist !next gl)
+  | (IPatSimpl _ | IPatClear _ as ipat) :: ipats ->
+       ipat :: eqmoveipats eqpat ipats
+  | (IPatAnon All :: _ | []) as ipats ->
+       IPatAnon One :: eqpat :: ipats
+  | ipat :: ipats ->
+       ipat :: eqpat :: ipats
+
+let ssrsmovetac = Goal.enter begin fun g ->
+  let sigma, concl = Goal.(sigma g, concl g) in
+  match EConstr.kind sigma concl with
+  | Term.Prod _ | Term.LetIn _ -> tclUNIT ()
+  | _ -> Tactics.hnf_in_concl
+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
+  | _::_ as view, (_, ({ gens = lastgen :: gens; clr }, ipats)) ->
+     let gentac = V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, [])) in
+     let conclusion _ t clear ccl =
+       Tactics.apply_type ~typecheck:true ccl [t] <*>
+       Tactics.clear (List.map Ssrcommon.hyp_id clear) in
+     gentac <*>
+     tclLAST_GEN ~to_ind:false lastgen
+       (tacVIEW_THEN_GRAB view ~conclusion) <*>
+     tclIPAT (IPatClear clr :: ipats)
+  | _::_ as view, (_, ({ gens = []; clr }, ipats)) ->
+     tclIPAT (IPatView view :: IPatClear clr :: ipats)
   | _, (Some pat, (dgens, ipats)) ->
-    let dgentac = with_dgens dgens eqmovetac ist in
-    tclTHEN dgentac (introstac ~ist (eqmoveipats pat ipats))
-  | _, (_, (([gens], clr), ipats)) ->
-    let gentac = genstac (gens, clr) ist in
-    tclTHEN gentac (introstac ~ist ipats)
-  | _, (_, ((_, clr), ipats)) ->
-    tclTHENLIST [movehnftac; cleartac clr; introstac ~ist ipats]
-
-let ssrcasetac ist (view, (eqid, (dgens, ipats))) =
-  let ndefectcasetac view eqid ipats deps ((_, occ), _ as gen) ist gl =
-    let simple = (eqid = None && deps = [] && occ = None) in
-    let cl, c, clr, gl = pf_interp_gen ist gl true gen in
-    let _,vc, gl =
-      if view = [] then c,c, gl else pf_with_view_linear ist gl (false, view) cl c in
-    if simple && is_injection_case vc gl then
-      tclTHENLIST [perform_injection vc; cleartac clr; introstac ~ist ipats] gl
-    else 
-      (* macro for "case/v E: x" ---> "case E: x / (v x)" *)
-      let deps, clr, occ = 
-        if view <> [] && eqid <> None && deps = [] then [gen], [], None
-        else deps, clr, occ in
-      ssrelim ~is_case:true ~ist deps (`EConstr (clr,occ, vc)) eqid (elim_intro_tac ipats) gl
+    let dgentac = with_dgens dgens eqmovetac in
+    dgentac <*> tclIPAT (eqmoveipats pat ipats)
+  | _, (_, ({ gens = (_ :: _ as gens); dgens = []; clr}, ipats)) ->
+    let gentac = V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, clr)) in
+    gentac <*> tclIPAT ipats
+  | _, (_, ({ clr }, ipats)) ->
+    Tacticals.New.tclTHENLIST [ssrsmovetac; Tactics.clear (List.map Ssrcommon.hyp_id clr); tclIPAT ipats]
+
+(** [abstract: absvar gens] **************************************************)
+let rec is_Evar_or_CastedMeta sigma x =
+  EConstr.isEvar sigma x ||
+  EConstr.isMeta sigma x ||
+  (EConstr.isCast sigma x &&
+    is_Evar_or_CastedMeta sigma (pi1 (EConstr.destCast sigma x)))
+
+let occur_existential_or_casted_meta sigma c =
+  let rec occrec c = match EConstr.kind sigma c with
+    | Term.Evar _ -> raise Not_found
+    | Term.Cast (m,_,_) when EConstr.isMeta sigma m -> raise Not_found
+    | _ -> EConstr.iter sigma occrec c
   in
-  with_dgens dgens (ndefectcasetac view eqid ipats) ist
-
-let ssrapplytac ist (views, (_, ((gens, clr), intros))) =
-  tclINTROS ist (inner_ssrapplytac views gens clr) intros
-
+  try occrec c; false
+  with Not_found -> true
+
+let tacEXAMINE_ABSTRACT id = Ssrcommon.tacTYPEOF id >>= begin fun tid ->
+  Ssrcommon.tacMK_SSR_CONST "abstract" >>= fun abstract ->
+  Goal.enter_one ~__LOC__ begin fun g ->
+  let sigma, env = Goal.(sigma g, env g) in
+  let err () =
+    Ssrcommon.errorstrm
+      Pp.(strbrk"not a proper abstract constant: "++
+        Printer.pr_econstr_env env sigma id) in
+  if not (EConstr.isApp sigma tid) then err ();
+  let hd, args_id = EConstr.destApp sigma tid in
+  if not (EConstr.eq_constr_nounivs sigma hd abstract) then err ();
+  if Array.length args_id <> 3 then err ();
+  if not (is_Evar_or_CastedMeta sigma args_id.(2)) then
+    Ssrcommon.errorstrm Pp.(strbrk"abstract constant "++
+      Printer.pr_econstr_env env sigma id++str" already used");
+  tclUNIT (tid, args_id)
+end end
+
+let tacFIND_ABSTRACT_PROOF check_lock abstract_n =
+  Ssrcommon.tacMK_SSR_CONST "abstract" >>= fun abstract ->
+  Goal.enter_one ~__LOC__ begin fun g ->
+    let sigma, env = Goal.(sigma g, env g) in
+    let l = Evd.fold_undefined (fun e ei l ->
+      match EConstr.kind sigma (EConstr.of_constr ei.Evd.evar_concl) with
+      | Term.App(hd, [|ty; n; lock|])
+        when (not check_lock ||
+                   (occur_existential_or_casted_meta sigma ty &&
+                    is_Evar_or_CastedMeta sigma lock)) &&
+             EConstr.eq_constr_nounivs sigma hd abstract &&
+             EConstr.eq_constr_nounivs sigma n abstract_n -> e :: l
+      | _ -> l) sigma [] in
+    match l with
+    | [e] -> tclUNIT e
+    | _ -> Ssrcommon.errorstrm
+       Pp.(strbrk"abstract constant "++
+         Printer.pr_econstr_env env sigma abstract_n ++
+           strbrk" not found in the evar map exactly once. "++
+           strbrk"Did you tamper with it?")
+end
+
+let ssrabstract dgens =
+  let main _ (_,cid) = Goal.enter begin fun g ->
+    Ssrcommon.tacMK_SSR_CONST "abstract" >>= fun abstract ->
+    Ssrcommon.tacMK_SSR_CONST "abstract_key" >>= fun abstract_key ->
+    Ssrcommon.tacINTERP_CPATTERN cid >>= fun cid ->
+    let id = EConstr.mkVar (Option.get (Ssrmatching.id_of_pattern cid)) in
+    tacEXAMINE_ABSTRACT id >>= fun (idty, args_id) ->
+    let abstract_n = args_id.(1) in
+    tacFIND_ABSTRACT_PROOF true abstract_n >>= fun abstract_proof ->
+    let tacFIND_HOLE = Goal.enter_one ~__LOC__ begin fun g ->
+      let sigma, env, concl = Goal.(sigma g, env g, concl g) in
+      let t = args_id.(0) in
+      match EConstr.kind sigma t with
+      | (Term.Evar _ | Term.Meta _) -> Ssrcommon.tacUNIFY concl t <*> tclUNIT id
+      | Term.Cast(m,_,_)
+        when EConstr.isEvar sigma m || EConstr.isMeta sigma m ->
+          Ssrcommon.tacUNIFY concl t <*> tclUNIT id
+      | _ ->
+          Ssrcommon.errorstrm
+            Pp.(strbrk"abstract constant "++
+               Printer.pr_econstr_env env sigma abstract_n ++
+               strbrk" has an unexpected shape. Did you tamper with it?")
+      end in
+    tacFIND_HOLE >>= fun proof ->
+    Ssrcommon.tacUNIFY abstract_key args_id.(2) <*>
+    Ssrcommon.tacTYPEOF idty >>= fun _ ->
+    Unsafe.tclGETGOALS >>= fun goals ->
+    (* Here we jump in the proof tree: we move from the current goal to
+       the evar that inhabits the abstract variable with the current goal *)
+    Unsafe.tclSETGOALS
+      (goals @ [Proofview_monad.with_empty_state abstract_proof]) <*>
+    tclDISPATCH [
+      Tacticals.New.tclSOLVE [Tactics.apply proof];
+      Ssrcommon.unfold[abstract;abstract_key]
+    ]
+  end in
+  let interp_gens { gens } ~conclusion = Goal.enter begin fun g ->
+   Ssrcommon.tacSIGMA >>= fun gl0 ->
+     let open Ssrmatching in
+     let ipats = List.map (fun (_,cp) ->
+       match id_of_pattern (interp_cpattern gl0 cp None) with
+       | None -> IPatAnon One
+       | Some id -> IPatId id)
+       (List.tl gens) in
+     conclusion ipats
+  end in
+  interp_gens dgens ~conclusion:(fun ipats ->
+  with_dgens dgens main <*>
+  tclIPATssr ipats)
+
+module Internal = struct
+
+  let pf_find_abstract_proof b gl t =
+    let res = ref None in
+    let _ = V82.of_tactic (tacFIND_ABSTRACT_PROOF b (EConstr.of_constr t) >>= fun x -> res := Some x; tclUNIT ()) gl in
+    match !res with
+    | None -> assert false
+    | Some x -> x
+
+  let examine_abstract t gl =
+    let res = ref None in
+    let _ = V82.of_tactic (tacEXAMINE_ABSTRACT t >>= fun x -> res := Some x; tclUNIT ()) gl in
+    match !res with
+    | None -> assert false
+    | Some x -> x
+
+end
 
 (* vim: set filetype=ocaml foldmethod=marker: *)
diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli
index 6c36e67e8..d80d14c85 100644
--- a/plugins/ssr/ssripats.mli
+++ b/plugins/ssr/ssripats.mli
@@ -6,77 +6,43 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* This file implements:
+   - the [=>] tactical
+   - the [:] pseudo-tactical for move, case, elim and abstract
 
-open Ssrmatching_plugin
-open Ssrast
-open Ssrcommon
-
-type block_names = (int * EConstr.types array) option
-
-(* For case/elim with eq generation: args are elim_tac introeq_tac ipats
- * elim E : "=> ipats" where E give rise to introeq_tac *)
-val tclEQINTROS :
-           ?ind:block_names ref ->
-           ?ist:ist ->
-           v82tac ->
-           v82tac -> ssripats -> v82tac
-(* special case with no eq and tactic taking ist *)
-val tclINTROS :
-           ist ->
-           (ist -> v82tac) ->
-           ssripats -> v82tac
-
-(* move=> ipats *)
-val introstac : ?ist:ist -> ssripats -> v82tac
-
-val elim_intro_tac :
-  Ssrast.ssripats ->
-  ?ist:Tacinterp.interp_sign ->
-  [> `EConstr of 'a * 'b * EConstr.t ] ->
-  Ssrast.ssripat option ->
-  Tacmach.tactic ->
-  bool ->
-  Ssrast.ssrhyp list ->
-  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
-
-(* "move=> top; tac top; clear top" respecting the speed *)
-val with_top : (EConstr.t -> v82tac) -> tac_ctx tac_a
+   Putting these two features in the same file lets one hide much of the
+   interaction between [tac E:] and [=>] ([E] has to be processed by [=>],
+   not by [:]
+*)
 
-val ssrmovetac :
-  Ltac_plugin.Tacinterp.interp_sign ->
-  Ssrast.ssrterm list *
-    (Ssrast.ssripat option *
-       (((Ssrast.ssrdocc * Ssrmatching.cpattern) list
-        list * Ssrast.ssrclear) *
-          Ssrast.ssripats)) ->
-  Tacmach.tactic
-
-val movehnftac : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
-
-val with_dgens :
-  (Ssrast.ssrdocc * Ssrmatching.cpattern) list
-   list * Ssrast.ssrclear ->
-  ((Ssrast.ssrdocc * Ssrmatching.cpattern) list ->
-   Ssrast.ssrdocc * Ssrmatching.cpattern ->
-   Ltac_plugin.Tacinterp.interp_sign -> Tacmach.tactic) ->
-  Ltac_plugin.Tacinterp.interp_sign -> Tacmach.tactic
-
-val ssrcasetac :
-  Ltac_plugin.Tacinterp.interp_sign ->
-  Ssrast.ssrterm list *
-    (Ssrast.ssripat option *
-       (((Ssrast.ssrdocc * Ssrmatching.cpattern) list list * Ssrast.ssrclear) *
-          Ssrast.ssripats)) ->
-  Tacmach.tactic
-
-val ssrapplytac :
-  Tacinterp.interp_sign ->
-  Ssrast.ssrterm list *
-    ('a *
-       ((((Ssrast.ssrhyps option * Ssrmatching_plugin.Ssrmatching.occ) *
-            (Ssrast.ssrtermkind * Tacexpr.glob_constr_and_expr))
-           list list * Ssrast.ssrhyps) *
-          Ssrast.ssripats)) ->
-  Tacmach.tactic
+open Ssrast
 
+(* The => tactical *)
+val tclIPAT : ssripats -> unit Proofview.tactic
+
+(* As above but with the SSR exception: first case is dispatch *)
+val tclIPATssr : ssripats -> unit Proofview.tactic
+
+(* Wrappers to deal with : and eqn generation/naming:
+     [tac E: gens => ipats]
+   where [E] is injected into [ipats] (at the right place) and [gens] are
+   generalized before calling [tac] *)
+val ssrmovetac : ssrmovearg -> unit Proofview.tactic
+val ssrsmovetac : unit Proofview.tactic
+val ssrelimtac : ssrmovearg -> unit Proofview.tactic
+val ssrselimtoptac : unit Proofview.tactic
+val ssrcasetac : ssrmovearg -> unit Proofview.tactic
+val ssrscasetoptac : unit Proofview.tactic
+
+(* The implementation of abstract: is half here, for the [[: var ]]
+ * ipat, and in ssrfwd for the integration with [have] *)
+val ssrabstract : ssrdgens -> unit Proofview.tactic
+
+(* Handling of [[:var]], needed in ssrfwd. Since ssrfwd is still outside the
+ * tactic monad we export code with the V82 interface *)
+module Internal : sig
+val examine_abstract :
+  EConstr.t -> Goal.goal Evd.sigma -> EConstr.types * EConstr.t array
+val pf_find_abstract_proof :
+  bool -> Goal.goal Evd.sigma -> Constr.constr -> Evar.t
+end
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 0d8044f19..b482fdb32 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -18,28 +18,28 @@ open Tacarg
 open Term
 open Libnames
 open Tactics
-open Tacticals
 open Tacmach
-open Glob_term
 open Util
 open Tacexpr
 open Tacinterp
 open Pltac
 open Extraargs
 open Ppconstr
-open Printer
 
 open Misctypes
 open Decl_kinds
 open Constrexpr
 open Constrexpr_ops
 
+open Proofview
+open Proofview.Notations
+
 open Ssrprinters
 open Ssrcommon
 open Ssrtacticals
 open Ssrbwd
 open Ssrequality
-open Ssrelim
+open Ssripats
 
 (** Ssreflect load check. *)
 
@@ -120,7 +120,6 @@ open Ssrast
 let pr_id = Ppconstr.pr_id
 let pr_name = function Name id -> pr_id id | Anonymous -> str "_"
 let pr_spc () = str " "
-let pr_bar () = Pp.cut() ++ str "|"
 let pr_list = prlist_with_sep
 
 (**************************** ssrhyp **************************************) 
@@ -172,7 +171,6 @@ ARGUMENT EXTEND ssrhoi_id TYPED AS ssrhoirep PRINTED BY pr_ssrhoi
 END
 
 
-let pr_hyps = pr_list pr_spc pr_hyp
 let pr_ssrhyps _ _ _ = pr_hyps
 
 ARGUMENT EXTEND ssrhyps TYPED AS ssrhyp list PRINTED BY pr_ssrhyps
@@ -183,25 +181,12 @@ END
 (** Rewriting direction *)
 
 
-let pr_dir = function L2R -> str "->" | R2L -> str "<-"
 let pr_rwdir = function L2R -> mt() | R2L -> str "-"
 
 let wit_ssrdir = add_genarg "ssrdir" pr_dir
 
 (** Simpl switch *)
 
-
-let pr_simpl = function
-  | Simpl -1 -> str "/="
-  | Cut -1 -> str "//"
-  | Simpl n -> str "/" ++ int n ++ str "="
-  | Cut n -> str "/" ++ int n ++ str"/"
-  | SimplCut (-1,-1) -> str "//="
-  | SimplCut (n,-1) -> str "/" ++ int n ++ str "/="
-  | SimplCut (-1,n) -> str "//" ++ int n ++ str "="
-  | SimplCut (n,m) -> str "/" ++ int n ++ str "/" ++ int m ++ str "="
-  | Nop -> mt ()
-
 let pr_ssrsimpl _ _ _ = pr_simpl
 
 let wit_ssrsimplrep = add_genarg "ssrsimplrep" pr_simpl
@@ -292,8 +277,6 @@ ARGUMENT EXTEND ssrsimpl TYPED AS ssrsimplrep PRINTED BY pr_ssrsimpl
 | [ ] -> [ Nop ]
 END
 
-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_ssrclear _ _ _ = pr_clear mt
 
@@ -429,7 +412,7 @@ ARGUMENT EXTEND ssrdocc TYPED AS ssrclear option * ssrocc PRINTED BY pr_ssrdocc
 | [ "{" ssrocc(occ) "}" ] -> [ mkocc occ ]
 END
 
-(* kinds of terms *)
+(* Old kinds of terms *)
 
 let input_ssrtermkind strm = match Util.stream_nth 0 strm with
   | Tok.KEYWORD "(" -> xInParens
@@ -438,12 +421,21 @@ let input_ssrtermkind strm = match Util.stream_nth 0 strm with
 
 let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind
 
+(* New kinds of terms *)
+
+let input_term_annotation strm =
+  match Stream.npeek 2 strm with
+  | Tok.KEYWORD "(" :: Tok.KEYWORD "(" :: _ -> `DoubleParens
+  | Tok.KEYWORD "(" :: _ -> `Parens
+  | Tok.KEYWORD "@" :: _ -> `At
+  | _ -> `None
+let term_annotation =
+  Gram.Entry.of_parser "term_annotation" input_term_annotation
+
 (* terms *)
 
 (** Terms parsing. ********************************************************)
 
-let interp_constr = interp_wit wit_constr
-
 (* Because we allow wildcards in term references, we need to stage the *)
 (* interpretation of terms so that it occurs at the right time during  *)
 (* the execution of the tactic (e.g., so that we don't report an error *)
@@ -452,9 +444,8 @@ let interp_constr = interp_wit wit_constr
 (* started with an opening paren, which might avoid a conflict between *)
 (* the ssrreflect term syntax and Gallina notation.                    *)
 
-(* terms *)
+(* Old terms *)
 let pr_ssrterm _ _ _ = pr_term
-let force_term ist gl (_, c) = interp_constr ist gl c
 let glob_ssrterm gs = function
   | k, (_, Some c) -> k, Tacintern.intern_constr gs c
   | ct -> ct
@@ -478,27 +469,71 @@ GEXTEND Gram
   ssrterm: [[ k = ssrtermkind; c = Pcoq.Constr.constr -> mk_term k c ]];
 END
 
-(* Views *)
+(* New terms *)
+
+let pp_ast_closure_term _ _ _ = pr_ast_closure_term
+
+ARGUMENT EXTEND ast_closure_term
+     PRINTED BY pp_ast_closure_term
+     INTERPRETED BY interp_ast_closure_term
+     GLOBALIZED BY glob_ast_closure_term
+     SUBSTITUTED BY subst_ast_closure_term
+     RAW_PRINTED BY pp_ast_closure_term
+     GLOB_PRINTED BY pp_ast_closure_term
+  | [ term_annotation(a) constr(c) ] -> [ mk_ast_closure_term a c ]
+END
+ARGUMENT EXTEND ast_closure_lterm
+     PRINTED BY pp_ast_closure_term
+     INTERPRETED BY interp_ast_closure_term
+     GLOBALIZED BY glob_ast_closure_term
+     SUBSTITUTED BY subst_ast_closure_term
+     RAW_PRINTED BY pp_ast_closure_term
+     GLOB_PRINTED BY pp_ast_closure_term
+  | [ term_annotation(a) lconstr(c) ] -> [ mk_ast_closure_term a c ]
+END
+
+(* Old Views *)
 
 let pr_view = pr_list mt (fun c -> str "/" ++ pr_term c)
 
-let pr_ssrview _ _ _ = pr_view
+let pr_ssrbwdview _ _ _ = pr_view
 
-ARGUMENT EXTEND ssrview TYPED AS ssrterm list
-   PRINTED BY pr_ssrview
+ARGUMENT EXTEND ssrbwdview TYPED AS ssrterm list
+   PRINTED BY pr_ssrbwdview
 | [ "YouShouldNotTypeThis" ] -> [ [] ]
 END
 
 Pcoq.(
 GEXTEND Gram
-  GLOBAL: ssrview;
-  ssrview: [
+  GLOBAL: ssrbwdview;
+  ssrbwdview: [
     [  test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr -> [mk_term xNoFlag c]
-    |  test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr; w = ssrview ->
+    |  test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr; w = ssrbwdview ->
                     (mk_term xNoFlag c) :: w ]];
 END
 )
 
+(* New Views *)
+
+
+let pr_ssrfwdview _ _ _ = pr_view2
+
+ARGUMENT EXTEND ssrfwdview TYPED AS ast_closure_term list
+   PRINTED BY pr_ssrfwdview
+| [ "YouShouldNotTypeThis" ] -> [ [] ]
+END
+
+Pcoq.(
+GEXTEND Gram
+  GLOBAL: ssrfwdview;
+  ssrfwdview: [
+    [  test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr ->
+            [mk_ast_closure_term `None c]
+    |  test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr; w = ssrfwdview ->
+                    (mk_ast_closure_term `None c) :: w ]];
+END
+)
+
 (* }}} *)
  
 (* ipats *)
@@ -531,24 +566,16 @@ let ipat_of_intro_pattern p = Misctypes.(
   ipat_of_intro_pattern p
 )
 
-let rec pr_ipat p =
-  match p with
-  | IPatId id -> pr_id id
-  | IPatSimpl sim -> pr_simpl sim
-  | IPatClear clr -> pr_clear mt clr
-  | IPatCase iorpat -> hov 1 (str "[" ++ pr_iorpat iorpat ++ 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 v -> pr_view v
-  | IPatNoop -> str "-"
-  | IPatNewHidden l -> str "[:" ++ pr_list spc pr_id l ++ str "]"
-(* TODO  | IPatAnon Temporary -> str "+" *)
-
-and pr_iorpat iorpat = pr_list pr_bar pr_ipats iorpat
-and pr_ipats ipats = pr_list spc pr_ipat ipats
+let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function
+  | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop) 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 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)
+  | IPatTac _ -> assert false (*internal usage only *)
 
 let wit_ssripatrep = add_genarg "ssripatrep" pr_ipat
 
@@ -556,13 +583,22 @@ let pr_ssripat _ _ _ = pr_ipat
 let pr_ssripats _ _ _ = pr_ipats
 let pr_ssriorpat _ _ _ = pr_iorpat
 
+(*
 let intern_ipat ist ipat =
   let rec check_pat = function
   | IPatClear clr -> ignore (List.map (intern_hyp ist) clr)
   | IPatCase iorpat -> List.iter (List.iter check_pat) iorpat
+  | IPatDispatch iorpat -> List.iter (List.iter check_pat) iorpat
   | IPatInj iorpat -> List.iter (List.iter check_pat) iorpat
   | _ -> () in
   check_pat ipat; ipat
+*)
+
+let intern_ipat ist =
+  map_ipat
+    (fun id -> id)
+    (intern_hyp ist) (* TODO: check with ltac, old code was ignoring the result *)
+    (glob_ast_closure_term ist)
 
 let intern_ipats ist = List.map (intern_ipat ist)
 
@@ -573,6 +609,10 @@ let interp_introid ist gl id = Misctypes.(
  with _ -> snd(snd (interp_intro_pattern ist gl (Loc.tag @@ IntroNaming (IntroIdentifier id))))
 )
 
+let get_intro_id = function
+  | IntroNaming (IntroIdentifier id) -> id
+  | _ -> assert false
+
 let rec add_intro_pattern_hyps (loc, ipat) hyps = Misctypes.(
   match ipat with
   | IntroNaming (IntroIdentifier id) ->
@@ -593,12 +633,14 @@ let rec add_intro_pattern_hyps (loc, ipat) hyps = Misctypes.(
       of ipat interp_introid could return [HH] *) assert false
 )
 
-(* MD: what does this do? *)
-let interp_ipat ist gl = Misctypes.(
+(* We interp the ipat using the standard ltac machinery for ids, since
+ * we have no clue what a name could be bound to (maybe another ipat) *)
+let interp_ipat ist gl =
   let ltacvar id = Id.Map.mem id ist.Tacinterp.lfun in
   let rec interp = function
   | IPatId id when ltacvar id ->
     ipat_of_intro_pattern (interp_introid ist gl id)
+  | IPatId _ as x -> x
   | IPatClear clr ->
     let add_hyps (SsrHyp (loc, id) as hyp) hyps =
       if not (ltacvar id) then hyp :: hyps else
@@ -607,16 +649,17 @@ let interp_ipat ist gl = Misctypes.(
     check_hyps_uniq [] clr'; IPatClear clr'
   | IPatCase(iorpat) ->
       IPatCase(List.map (List.map interp) iorpat)
+  | IPatDispatch(iorpat) ->
+      IPatDispatch(List.map (List.map interp) iorpat)
   | IPatInj iorpat -> IPatInj (List.map (List.map interp) iorpat)
-  | IPatNewHidden l ->
-      IPatNewHidden
-        (List.map (function
-           | IntroNaming (IntroIdentifier id) -> id
-           | _ -> assert false)
-        (List.map (interp_introid ist gl) l))
-  | ipat -> ipat in
+  | 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
+     gl x)) l)
+  | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop) as x -> x
+  | IPatTac _ -> assert false (*internal usage only *)
+    in
   interp
-)
 
 let interp_ipats ist gl l = project gl, List.map (interp_ipat ist gl) l
 
@@ -670,9 +713,9 @@ 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))] ]
-  | [ ssrview(v) ] -> [ [IPatView v] ]
-  | [ "[" ":" ident_list(idl) "]" ] -> [ [IPatNewHidden idl] ]
-  | [ "[:" ident_list(idl) "]" ] -> [ [IPatNewHidden idl] ]
+  | [ ssrfwdview(v) ] -> [ [IPatView v] ]
+  | [ "[" ":" ident_list(idl) "]" ] -> [ [IPatAbstractVars idl] ]
+  | [ "[:" ident_list(idl) "]" ] -> [ [IPatAbstractVars idl] ]
 END
 
 ARGUMENT EXTEND ssripats TYPED AS ssripat PRINTED BY pr_ssripats
@@ -713,6 +756,12 @@ GEXTEND Gram
 (*      check_no_inner_seed !@loc false iorpat;
       IPatCase (understand_case_type iorpat) *)
       IPatCase iorpat
+(*
+   | test_nohidden; "("; iorpat = ssriorpat; ")" ->
+(*      check_no_inner_seed !@loc false iorpat;
+      IPatCase (understand_case_type iorpat) *)
+      IPatDispatch iorpat
+*)
    | test_nohidden; "[="; iorpat = ssriorpat; "]" ->
 (*      check_no_inner_seed !@loc false iorpat; *)
       IPatInj iorpat ]];
@@ -750,7 +799,7 @@ let check_ssrhpats loc w_binders ipats =
   let ipat, binders =
     let rec loop ipat = function
       | [] -> ipat, []
-      | ( IPatId _| IPatAnon _| IPatCase _| IPatRewrite _ as i) :: tl -> 
+      | ( IPatId _| IPatAnon _| IPatCase _ | IPatDispatch _ | IPatRewrite _ as i) :: tl ->
         if w_binders then
           if simpl <> [] && tl <> [] then 
             err_loc(str"binders XOR s-item allowed here: "++pr_ipats(tl@simpl))
@@ -818,8 +867,8 @@ END
 TACTIC EXTEND ssrtclintros
 | [ "YouShouldNotTypeThis" ssrintrosarg(arg) ] ->
   [ let tac, intros = arg in
-    Proofview.V82.tactic (Ssripats.tclINTROS ist (fun ist -> ssrevaltac ist tac) intros) ]
-    END
+    ssrevaltac ist tac <*> tclIPATssr intros ]
+END
 
 (** Defined identifier *)
 let pr_ssrfwdid id = pr_spc () ++ pr_id id
@@ -1004,15 +1053,6 @@ let pr_binder prl = function
   | Bcast t ->
     str ": " ++ prl t
 
-let rec mkBstruct i = function
-  | Bvar x :: b ->
-    if i = 0 then [Bstruct x] else mkBstruct (i - 1) b
-  | Bdecl (xs, _) :: b ->
-    let i' = i - List.length xs in
-    if i' < 0 then [Bstruct (List.nth xs i)] else mkBstruct i' b
-  | _ :: b -> mkBstruct i b
-  | [] -> []
-
 let rec format_local_binders h0 bl0 = match h0, bl0 with
   | BFvar :: h, CLocalAssum ([{CAst.v=x}], _,  _) :: bl ->
     Bvar x :: format_local_binders h bl
@@ -1044,51 +1084,6 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with
   | _, c ->
     [], c
 
-let rec format_glob_decl h0 d0 = match h0, d0 with
-  | BFvar :: h, (x, _, None, _) :: d ->
-    Bvar x :: format_glob_decl h d
-  | BFdecl 1 :: h,  (x, _, None, t) :: d ->
-    Bdecl ([x], t) :: format_glob_decl h d
-  | BFdecl n :: h, (x, _, None, t) :: d when n > 1 ->
-    begin match format_glob_decl (BFdecl (n - 1) :: h) d with
-    | Bdecl (xs, _) :: bs -> Bdecl (x :: xs, t) :: bs
-    | bs -> Bdecl ([x], t) :: bs
-    end
-  | BFdef :: h, (x, _, Some v, _)  :: d ->
-    Bdef (x, None, v) :: format_glob_decl h d
-  | _, (x, _, None, t) :: d ->
-    Bdecl ([x], t) :: format_glob_decl [] d
-  | _, (x, _, Some v, _) :: d ->
-     Bdef (x, None, v) :: format_glob_decl [] d
-  | _, [] -> []
-
-let rec format_glob_constr h0 c0 = match h0, DAst.get c0 with
-  | BFvar :: h, GLambda (x, _, _, c) ->
-    let bs, c' = format_glob_constr h c in
-    Bvar x :: bs, c'
-  | BFdecl 1 :: h, GLambda (x, _, t, c) ->
-    let bs, c' = format_glob_constr h c in
-    Bdecl ([x], t) :: bs, c'
-  | BFdecl n :: h, GLambda (x, _, t, c) when n > 1 ->
-    begin match format_glob_constr (BFdecl (n - 1) :: h) c with
-    | Bdecl (xs, _) :: bs, c' -> Bdecl (x :: xs, t) :: bs, c'
-    | _ -> [Bdecl ([x], t)], c
-    end
-  | BFdef :: h, GLetIn(x, v, oty, c) ->
-    let bs, c' = format_glob_constr h c in
-    Bdef (x, oty, v) :: bs, c'
-  | [BFcast], GCast (c, CastConv t) ->
-    [Bcast t], c
-  | BFrec (has_str, has_cast) :: h, GRec (f, _, bl, t, c)
-      when Array.length c = 1 ->
-    let bs = format_glob_decl h bl.(0) in
-    let bstr = match has_str, f with
-    | true, GFix ([|Some i, GStructRec|], _) -> mkBstruct i bs
-    | _ -> [] in
-    bs @ bstr @ (if has_cast then [Bcast t.(0)] else []), c.(0)
-  | _, _ ->
-    [], c0
-
 (** Forward chaining argument *)
 
 (* There are three kinds of forward definitions:           *)
@@ -1104,19 +1099,32 @@ let wit_ssrfwdfmt = add_genarg "ssrfwdfmt" pr_fwdfmt
 
 (* type ssrfwd = ssrfwdfmt * ssrterm *)
 
-let mkFwdVal fk c = ((fk, []), mk_term xNoFlag c)
+let mkFwdVal fk c = ((fk, []), c)
 let mkssrFwdVal fk c = ((fk, []), (c,None))
 let dC t = CastConv t
 
-let mkFwdCast fk ?loc t c = ((fk, [BFcast]), mk_term ' ' (CAst.make ?loc @@ CCast (c, dC t)))
+let same_ist { interp_env = x } { interp_env = y } =
+  match x,y with
+  | None, None -> true
+  | Some a, Some b -> a == b
+  | _ -> false
+
+let mkFwdCast fk ?loc ?c t =
+  let c = match c with
+    | None -> mkCHole loc
+    | Some c -> assert (same_ist t c); c.body in
+  ((fk, [BFcast]),
+   { t with annotation = `None;
+            body = (CAst.make ?loc @@ CCast (c, dC t.body)) })
+
 let mkssrFwdCast fk loc t c = ((fk, [BFcast]), (c, Some t))
 
 let mkFwdHint s t =
-  let loc =  Constrexpr_ops.constr_loc t in
-  mkFwdCast (FwdHint (s,false)) ?loc t (mkCHole loc)
+  let loc =  Constrexpr_ops.constr_loc t.body in
+  mkFwdCast (FwdHint (s,false)) ?loc t
 let mkFwdHintNoTC s t =
-  let loc =  Constrexpr_ops.constr_loc t in
-  mkFwdCast (FwdHint (s,true)) ?loc t (mkCHole loc)
+  let loc =  Constrexpr_ops.constr_loc t.body in
+  mkFwdCast (FwdHint (s,true)) ?loc t
 
 let pr_gen_fwd prval prc prlc fk (bs, c) =
   let prc s = str s ++ spc () ++ prval prc prlc c in
@@ -1128,19 +1136,17 @@ let pr_gen_fwd prval prc prlc fk (bs, c) =
   | _, _ -> spc () ++ pr_list spc (pr_binder prlc) bs ++ prc " :="
 
 let pr_fwd_guarded prval prval' = function
-| (fk, h), (_, (_, Some c)) ->
-  pr_gen_fwd prval pr_constr_expr prl_constr_expr fk (format_constr_expr h c)
-| (fk, h), (_, (c, None)) ->
-  pr_gen_fwd prval' pr_glob_constr_env prl_glob_constr fk (format_glob_constr h c)
+| (fk, h), c ->
+  pr_gen_fwd prval pr_constr_expr prl_constr_expr fk (format_constr_expr h c.body)
 
 let pr_unguarded prc prlc = prlc
 
 let pr_fwd = pr_fwd_guarded pr_unguarded pr_unguarded
 let pr_ssrfwd _ _ _ = pr_fwd
  
-ARGUMENT EXTEND ssrfwd TYPED AS (ssrfwdfmt * ssrterm) PRINTED BY pr_ssrfwd
-  | [ ":=" lconstr(c) ] -> [ mkFwdVal FwdPose c ]
-  | [ ":" lconstr (t) ":=" lconstr(c) ] -> [ mkFwdCast FwdPose ~loc t c ]
+ARGUMENT EXTEND ssrfwd TYPED AS (ssrfwdfmt * ast_closure_lterm) PRINTED BY pr_ssrfwd
+  | [ ":=" ast_closure_lterm(c) ] -> [ mkFwdVal FwdPose c ]
+  | [ ":" ast_closure_lterm (t) ":=" ast_closure_lterm(c) ] -> [ mkFwdCast FwdPose ~loc t ~c ]
 END
 
 (** Independent parsing for binders *)
@@ -1236,10 +1242,8 @@ END
 
 (* The plain pose form. *)
 
-let bind_fwd bs = function
-  | (fk, h), (ck, (rc, Some c)) ->
-    (fk,binders_fmts bs @ h), (ck,(rc,Some (push_binders c bs)))
-  | fwd -> fwd
+let bind_fwd bs ((fk, h), c) =
+ (fk,binders_fmts bs @ h), { c with body = push_binders c.body bs }
 
 ARGUMENT EXTEND ssrposefwd TYPED AS ssrfwd PRINTED BY pr_ssrfwd
   | [ ssrbinder_list(bs) ssrfwd(fwd) ] -> [ bind_fwd bs fwd ]
@@ -1257,8 +1261,8 @@ let bvar_locid = function
 ARGUMENT EXTEND ssrfixfwd TYPED AS ident * ssrfwd PRINTED BY pr_ssrfixfwd
   | [ "fix" ssrbvar(bv) ssrbinder_list(bs) ssrstruct(sid) ssrfwd(fwd) ] ->
     [ let { CAst.v=id } as lid = bvar_locid bv in
-      let (fk, h), (ck, (rc, oc)) = fwd in
-      let c = Option.get oc in
+      let (fk, h), ac = fwd in
+      let c = ac.body in
       let has_cast, t', c' = match format_constr_expr h c with
       | [Bcast t'], c' -> true, t', c'
       | _ -> false, mkCHole (constr_loc c), c in
@@ -1274,7 +1278,7 @@ ARGUMENT EXTEND ssrfixfwd TYPED AS ident * ssrfwd PRINTED BY pr_ssrfixfwd
         loop (names_of_local_assums lb) in
       let h' = BFrec (has_struct, has_cast) :: binders_fmts bs in
       let fix = CAst.make ~loc @@ CFix (lid, [lid, (Some i, CStructRec), lb, t', c']) in
-      id, ((fk, h'), (ck, (rc, Some fix))) ]
+      id, ((fk, h'),  { ac with body = fix }) ]
 END
 
 
@@ -1285,14 +1289,14 @@ let pr_ssrcofixfwd _ _ _ (id, fwd) = str " cofix " ++ pr_id id ++ pr_fwd fwd
 ARGUMENT EXTEND ssrcofixfwd TYPED AS ssrfixfwd PRINTED BY pr_ssrcofixfwd
   | [ "cofix" ssrbvar(bv) ssrbinder_list(bs) ssrfwd(fwd) ] ->
     [ let { CAst.v=id } as lid = bvar_locid bv in
-      let (fk, h), (ck, (rc, oc)) = fwd in
-      let c = Option.get oc in
+      let (fk, h), ac = fwd in
+      let c = ac.body in
       let has_cast, t', c' = match format_constr_expr h c with
       | [Bcast t'], c' -> true, t', c'
       | _ -> false, mkCHole (constr_loc c), c in
       let h' = BFrec (false, has_cast) :: binders_fmts bs in
       let cofix = CAst.make ~loc @@ CCoFix (lid, [lid, fix_binders bs, t', c']) in
-      id, ((fk, h'), (ck, (rc, Some cofix)))
+      id, ((fk, h'), { ac with body = cofix })
     ]
 END
 
@@ -1302,12 +1306,12 @@ let pr_ssrsetfwd _ _ _ (((fk,_),(t,_)), docc) =
     (fun _ -> mt()) (fun _ -> mt()) fk ([Bcast ()],t)
 
 ARGUMENT EXTEND ssrsetfwd
-TYPED AS (ssrfwdfmt * (lcpattern * ssrterm option)) * ssrdocc
+TYPED AS (ssrfwdfmt * (lcpattern * ast_closure_lterm option)) * ssrdocc
 PRINTED BY pr_ssrsetfwd
-| [ ":" lconstr(t) ":=" "{" ssrocc(occ) "}" cpattern(c) ] ->
-  [ mkssrFwdCast FwdPose loc (mk_lterm t) c, mkocc occ ]
-| [ ":" lconstr(t) ":=" lcpattern(c) ] ->
-  [ mkssrFwdCast FwdPose loc (mk_lterm t) c, nodocc ]
+| [ ":" ast_closure_lterm(t) ":=" "{" ssrocc(occ) "}" cpattern(c) ] ->
+  [ mkssrFwdCast FwdPose loc t c, mkocc occ ]
+| [ ":" ast_closure_lterm(t) ":=" lcpattern(c) ] ->
+  [ mkssrFwdCast FwdPose loc t c, nodocc ]
 | [ ":=" "{" ssrocc(occ) "}" cpattern(c) ] ->
   [ mkssrFwdVal FwdPose c, mkocc occ ]
 | [ ":=" lcpattern(c) ] -> [ mkssrFwdVal FwdPose c, nodocc ]
@@ -1317,10 +1321,10 @@ END
 let pr_ssrhavefwd _ _ prt (fwd, hint) = pr_fwd fwd ++ pr_hint prt hint
 
 ARGUMENT EXTEND ssrhavefwd TYPED AS ssrfwd * ssrhint PRINTED BY pr_ssrhavefwd
-| [ ":" lconstr(t) ssrhint(hint) ] -> [ mkFwdHint ":" t, hint ]
-| [ ":" lconstr(t) ":=" lconstr(c) ] -> [ mkFwdCast FwdHave ~loc t c, nohint ]
-| [ ":" lconstr(t) ":=" ] -> [ mkFwdHintNoTC ":" t, nohint ]
-| [ ":=" lconstr(c) ] -> [ mkFwdVal FwdHave c, nohint ]
+| [ ":" ast_closure_lterm(t) ssrhint(hint) ] -> [ mkFwdHint ":" t, hint ]
+| [ ":" ast_closure_lterm(t) ":=" ast_closure_lterm(c) ] -> [ mkFwdCast FwdHave ~loc t ~c, nohint ]
+| [ ":" ast_closure_lterm(t) ":=" ] -> [ mkFwdHintNoTC ":" t, nohint ]
+| [ ":=" ast_closure_lterm(c) ] -> [ mkFwdVal FwdHave c, nohint ]
 END
 
 let intro_id_to_binder = List.map (function 
@@ -1429,7 +1433,7 @@ let tactic_expr = Pltac.tactic_expr
 (* debug *)
 
 (* Let's play with the new proof engine API *)
-let old_tac = Proofview.V82.tactic
+let old_tac = V82.tactic
 
 
 (** Name generation {{{ *******************************************************)
@@ -1559,12 +1563,12 @@ let ssrautoprop gl =
       try Tacenv.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop"))
       with Not_found -> Tacenv.locate_tactic (ssrqid "ssrautoprop") in
     let tacexpr = Loc.tag @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
-    Proofview.V82.of_tactic (eval_tactic (Tacexpr.TacArg tacexpr)) gl
-  with Not_found -> Proofview.V82.of_tactic (Auto.full_trivial []) gl
+    V82.of_tactic (eval_tactic (Tacexpr.TacArg tacexpr)) gl
+  with Not_found -> V82.of_tactic (Auto.full_trivial []) gl
 
 let () = ssrautoprop_tac := ssrautoprop
 
-let tclBY tac = tclTHEN tac (donetac ~-1)
+let tclBY tac = Tacticals.tclTHEN tac (donetac ~-1)
 
 (** Tactical arguments. *)
 
@@ -1580,7 +1584,7 @@ let tclBY tac = tclTHEN tac (donetac ~-1)
 open Ssrfwd
 
 TACTIC EXTEND ssrtclby
-| [ "by" ssrhintarg(tac) ] -> [ Proofview.V82.tactic (hinttac ist true tac) ]
+| [ "by" ssrhintarg(tac) ] -> [ V82.tactic (hinttac ist true tac) ]
 END
 
 (* }}} *)
@@ -1592,15 +1596,13 @@ GEXTEND Gram
   ssrhint: [[ "by"; arg = ssrhintarg -> arg ]];
 END
 
-open Ssripats
-
 (** The "do" tactical. ********************************************************)
 
 (*
 type ssrdoarg = ((ssrindex * ssrmmod) * ssrhint) * ssrclauses
 *)
 TACTIC EXTEND ssrtcldo
-| [ "YouShouldNotTypeThis" "do" ssrdoarg(arg) ] -> [ Proofview.V82.tactic (ssrdotac ist arg) ]
+| [ "YouShouldNotTypeThis" "do" ssrdoarg(arg) ] -> [ V82.tactic (ssrdotac ist arg) ]
 END
 set_pr_ssrtac "tcldo" 3 [ArgSep "do "; ArgSsr "doarg"]
 
@@ -1639,7 +1641,7 @@ END
 
 TACTIC EXTEND ssrtclseq
 | [ "YouShouldNotTypeThis" ssrtclarg(tac) ssrseqdir(dir) ssrseqarg(arg) ] ->
-  [ Proofview.V82.tactic (tclSEQAT ist tac dir arg) ]
+  [ V82.tactic (tclSEQAT ist tac dir arg) ]
 END
 set_pr_ssrtac "tclseq" 5 [ArgSsr "tclarg"; ArgSsr "seqdir"; ArgSsr "seqarg"]
 
@@ -1792,17 +1794,17 @@ END
 (* the entry point parses only non-empty arguments to avoid conflicts  *)
 (* with the basic Coq tactics.                                         *)
 
-(* type ssrarg = ssrview * (ssreqid * (ssrdgens * ssripats)) *)
+(* type ssrarg = ssrbwdview * (ssreqid * (ssrdgens * ssripats)) *)
 
 let pr_ssrarg _ _ _ (view, (eqid, (dgens, ipats))) =
   let pri = pr_intros (gens_sep dgens) in
-  pr_view view ++ pr_eqid eqid ++ pr_dgens pr_gen dgens ++ pri ipats
+  pr_view2 view ++ pr_eqid eqid ++ pr_dgens pr_gen dgens ++ pri ipats
 
-ARGUMENT EXTEND ssrarg TYPED AS ssrview * (ssreqid * (ssrdgens * ssrintros))
+ARGUMENT EXTEND ssrarg TYPED AS ssrfwdview * (ssreqid * (ssrdgens * ssrintros))
    PRINTED BY pr_ssrarg
-| [ ssrview(view) ssreqid(eqid) ssrdgens(dgens) ssrintros(ipats) ] ->
+| [ ssrfwdview(view) ssreqid(eqid) ssrdgens(dgens) ssrintros(ipats) ] ->
   [ view, (eqid, (dgens, ipats)) ]
-| [ ssrview(view) ssrclear(clr) ssrintros(ipats) ] ->
+| [ ssrfwdview(view) ssrclear(clr) ssrintros(ipats) ] ->
   [ view, (None, (([], clr), ipats)) ]
 | [ ssreqid(eqid) ssrdgens(dgens) ssrintros(ipats) ] ->
   [ [], (eqid, (dgens, ipats)) ]
@@ -1816,10 +1818,8 @@ END
 
 (* We just add a numeric version that clears the n top assumptions. *)
 
-let poptac ist n = introstac ~ist (List.init n (fun _ -> IPatAnon Drop))
-
 TACTIC EXTEND ssrclear
-  | [ "clear" natural(n) ] -> [ Proofview.V82.tactic (poptac ist n) ]
+  | [ "clear" natural(n) ] -> [ tclIPAT (List.init n (fun _ -> IPatAnon Drop)) ]
 END
 
 (** The "move" tactic *)
@@ -1827,7 +1827,7 @@ END
 (* TODO: review this, in particular the => _ and => [] cases *)
 let rec improper_intros = function
   | IPatSimpl _ :: ipats -> improper_intros ipats
-  | (IPatId _ | IPatAnon _ | IPatCase _) :: _ -> false
+  | (IPatId _ | IPatAnon _ | IPatCase _ | IPatDispatch _) :: _ -> false
   | _ -> true (* FIXME *)
 
 let check_movearg = function
@@ -1845,15 +1845,16 @@ ARGUMENT EXTEND ssrmovearg TYPED AS ssrarg PRINTED BY pr_ssrarg
 | [ ssrarg(arg) ] -> [ check_movearg arg ]
 END
 
-
+let movearg_of_parsed_movearg (v,(eq,(dg,ip))) =
+  (v,(eq,(ssrdgens_of_parsed_dgens dg,ip)))
 
 TACTIC EXTEND ssrmove
 | [ "move" ssrmovearg(arg) ssrrpat(pat) ] ->
-  [ Proofview.V82.tactic (tclTHEN (ssrmovetac ist arg) (introstac ~ist [pat])) ]
+  [ ssrmovetac (movearg_of_parsed_movearg arg) <*> tclIPAT [pat] ]
 | [ "move" ssrmovearg(arg) ssrclauses(clauses) ] ->
-  [ Proofview.V82.tactic (tclCLAUSES ist (ssrmovetac ist arg) clauses) ]
-| [ "move" ssrrpat(pat) ] -> [ Proofview.V82.tactic (introstac ~ist [pat]) ]
-| [ "move" ] -> [ Proofview.V82.tactic (movehnftac) ]
+  [ tclCLAUSES (ssrmovetac (movearg_of_parsed_movearg arg)) clauses ]
+| [ "move" ssrrpat(pat) ] -> [ tclIPAT [pat] ]
+| [ "move" ] -> [ ssrsmovetac ]
 END
 
 let check_casearg = function
@@ -1865,31 +1866,18 @@ ARGUMENT EXTEND ssrcasearg TYPED AS ssrarg PRINTED BY pr_ssrarg
 | [ ssrarg(arg) ] -> [ check_casearg arg ]
 END
 
-
 TACTIC EXTEND ssrcase
 | [ "case" ssrcasearg(arg) ssrclauses(clauses) ] ->
-  [ old_tac (tclCLAUSES ist (ssrcasetac ist arg) clauses) ]
-| [ "case" ] -> [ old_tac (with_fresh_ctx (with_top (ssrscasetac false))) ]
+  [ tclCLAUSES (ssrcasetac (movearg_of_parsed_movearg arg)) clauses ]
+| [ "case" ] -> [ ssrscasetoptac ]
 END
 
 (** The "elim" tactic *)
 
-(* Elim views are elimination lemmas, so the eliminated term is not addded *)
-(* to the dependent terms as for "case", unless it actually occurs in the  *)
-(* goal, the "all occurrences" {+} switch is used, or the equation switch  *)
-(* is used and there are no dependents.                                    *)
-
-let ssrelimtac ist (view, (eqid, (dgens, ipats))) =
-  let ndefectelimtac view eqid ipats deps gen ist gl =
-    let elim = match view with [v] -> Some (snd(force_term ist gl v)) | _ -> None in
-    ssrelim ~ist deps (`EGen gen) ?elim eqid (elim_intro_tac ipats) gl
-  in
-  with_dgens dgens (ndefectelimtac view eqid ipats) ist 
-
 TACTIC EXTEND ssrelim
 | [ "elim" ssrarg(arg) ssrclauses(clauses) ] ->
-  [ old_tac (tclCLAUSES ist (ssrelimtac ist arg) clauses) ]
-| [ "elim" ] -> [ old_tac (with_fresh_ctx (with_top elimtac)) ]
+  [ tclCLAUSES (ssrelimtac (movearg_of_parsed_movearg arg)) clauses ]
+| [ "elim" ] -> [ ssrselimtoptac ]
 END
 
 (** 6. Backward chaining tactics: apply, exact, congr. *)
@@ -1915,14 +1903,14 @@ PRINTED BY pr_ssragens
 | [ ] -> [ [[]], [] ]
 END
 
-let mk_applyarg views agens intros = views, (None, (agens, intros))
+let mk_applyarg views agens intros = views, (agens, intros)
 
-let pr_ssraarg _ _ _ (view, (eqid, (dgens, ipats))) =
+let pr_ssraarg _ _ _ (view, (dgens, ipats)) =
   let pri = pr_intros (gens_sep dgens) in
-  pr_view view ++ pr_eqid eqid ++ pr_dgens pr_agen dgens ++ pri ipats
+  pr_view view ++ pr_dgens pr_agen dgens ++ pri ipats
 
 ARGUMENT EXTEND ssrapplyarg 
-TYPED AS ssrview * (ssreqid * (ssragens * ssrintros))
+TYPED AS ssrbwdview * (ssragens * ssrintros)
 PRINTED BY pr_ssraarg
 | [ ":" ssragen(gen) ssragens(dgens) ssrintros(intros) ] ->
   [ mk_applyarg [] (cons_gen gen dgens) intros ]
@@ -1930,15 +1918,17 @@ PRINTED BY pr_ssraarg
   [ mk_applyarg [] ([], clr) intros ]
 | [ ssrintros_ne(intros) ] ->
   [ mk_applyarg [] ([], []) intros ]
-| [ ssrview(view) ":" ssragen(gen) ssragens(dgens) ssrintros(intros) ] ->
+| [ ssrbwdview(view) ":" ssragen(gen) ssragens(dgens) ssrintros(intros) ] ->
   [ mk_applyarg view (cons_gen gen dgens) intros ]
-| [ ssrview(view) ssrclear(clr) ssrintros(intros) ] ->
+| [ ssrbwdview(view) ssrclear(clr) ssrintros(intros) ] ->
   [ mk_applyarg view ([], clr) intros ]
     END
 
 TACTIC EXTEND ssrapply
-| [ "apply" ssrapplyarg(arg) ] -> [ Proofview.V82.tactic (ssrapplytac ist arg) ]
-| [ "apply" ] -> [ Proofview.V82.tactic apply_top_tac ]
+| [ "apply" ssrapplyarg(arg) ] -> [
+     let views, (gens_clr, intros) = arg in
+     inner_ssrapplytac views gens_clr ist <*> tclIPATssr intros ]
+| [ "apply" ] -> [ apply_top_tac ]
 END
 
 (** The "exact" tactic *)
@@ -1948,20 +1938,23 @@ let mk_exactarg views dgens = mk_applyarg views dgens []
 ARGUMENT EXTEND ssrexactarg TYPED AS ssrapplyarg PRINTED BY pr_ssraarg
 | [ ":" ssragen(gen) ssragens(dgens) ] ->
   [ mk_exactarg [] (cons_gen gen dgens) ]
-| [ ssrview(view) ssrclear(clr) ] ->
+| [ ssrbwdview(view) ssrclear(clr) ] ->
   [ mk_exactarg view ([], clr) ]
 | [ ssrclear_ne(clr) ] ->
   [ mk_exactarg [] ([], clr) ]
 END
 
 let vmexacttac pf =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Goal.nf_enter begin fun gl ->
   exact_no_check (EConstr.mkCast (pf, VMcast, Tacmach.New.pf_concl gl))
   end
 
 TACTIC EXTEND ssrexact
-| [ "exact" ssrexactarg(arg) ] -> [ Proofview.V82.tactic (tclBY (ssrapplytac ist arg)) ]
-| [ "exact" ] -> [ Proofview.V82.tactic (tclORELSE (donetac ~-1) (tclBY apply_top_tac)) ]
+| [ "exact" ssrexactarg(arg) ] -> [
+     let views, (gens_clr, _) = arg in
+     V82.tactic (tclBY (V82.of_tactic (inner_ssrapplytac views gens_clr ist))) ]
+| [ "exact" ] -> [
+     V82.tactic (Tacticals.tclORELSE (donetac ~-1) (tclBY (V82.of_tactic apply_top_tac))) ]
 | [ "exact" "<:" lconstr(pf) ] -> [ vmexacttac pf ]
 END
 
@@ -1986,9 +1979,9 @@ END
 TACTIC EXTEND ssrcongr
 | [ "congr" ssrcongrarg(arg) ] ->
 [ let arg, dgens = arg in
-  Proofview.V82.tactic begin
+  V82.tactic begin
     match dgens with
-    | [gens], clr -> tclTHEN (genstac (gens,clr) ist) (newssrcongrtac arg ist)
+    | [gens], clr -> Tacticals.tclTHEN (genstac (gens,clr)) (newssrcongrtac arg ist)
     | _ -> errorstrm (str"Dependent family abstractions not allowed in congr")
   end]
 END
@@ -2097,10 +2090,10 @@ ARGUMENT EXTEND ssrrwarg
 END
 
 TACTIC EXTEND ssrinstofruleL2R
-| [ "ssrinstancesofruleL2R" ssrterm(arg) ] -> [ Proofview.V82.tactic (ssrinstancesofrule ist L2R arg) ]
+| [ "ssrinstancesofruleL2R" ssrterm(arg) ] -> [ V82.tactic (ssrinstancesofrule ist L2R arg) ]
 END
 TACTIC EXTEND ssrinstofruleR2L
-| [ "ssrinstancesofruleR2L" ssrterm(arg) ] -> [ Proofview.V82.tactic (ssrinstancesofrule ist R2L arg) ]
+| [ "ssrinstancesofruleR2L" ssrterm(arg) ] -> [ V82.tactic (ssrinstancesofrule ist R2L arg) ]
 END
 
 (** Rewrite argument sequence *)
@@ -2141,7 +2134,7 @@ END
 
 TACTIC EXTEND ssrrewrite
   | [ "rewrite" ssrrwargs(args) ssrclauses(clauses) ] ->
-    [ Proofview.V82.tactic (tclCLAUSES ist (ssrrewritetac ist args) clauses) ]
+    [ tclCLAUSES (old_tac (ssrrewritetac ist args)) clauses ]
 END
 
 (** The "unlock" tactic *)
@@ -2164,16 +2157,16 @@ END
 
 TACTIC EXTEND ssrunlock
   | [ "unlock" ssrunlockargs(args) ssrclauses(clauses) ] ->
-[  Proofview.V82.tactic (tclCLAUSES ist (unlocktac ist args) clauses) ]
+    [ tclCLAUSES (old_tac (unlocktac ist args)) clauses ]
 END
 
 (** 8. Forward chaining tactics (pose, set, have, suffice, wlog) *)
 
 
 TACTIC EXTEND ssrpose
-| [ "pose" ssrfixfwd(ffwd) ] -> [ Proofview.V82.tactic (ssrposetac ist ffwd) ]
-| [ "pose" ssrcofixfwd(ffwd) ] -> [ Proofview.V82.tactic (ssrposetac ist ffwd) ]
-| [ "pose" ssrfwdid(id) ssrposefwd(fwd) ] -> [ Proofview.V82.tactic (ssrposetac ist (id, fwd)) ]
+| [ "pose" ssrfixfwd(ffwd) ] -> [ V82.tactic (ssrposetac ffwd) ]
+| [ "pose" ssrcofixfwd(ffwd) ] -> [ V82.tactic (ssrposetac ffwd) ]
+| [ "pose" ssrfwdid(id) ssrposefwd(fwd) ] -> [ V82.tactic (ssrposetac (id, fwd)) ]
 END
 
 (** The "set" tactic *)
@@ -2182,7 +2175,7 @@ END
 
 TACTIC EXTEND ssrset
 | [ "set" ssrfwdid(id) ssrsetfwd(fwd) ssrclauses(clauses) ] ->
-  [ Proofview.V82.tactic (tclCLAUSES ist (ssrsettac ist id fwd) clauses) ]
+  [ tclCLAUSES (old_tac (ssrsettac id fwd)) clauses ]
 END
 
 (** The "have" tactic *)
@@ -2204,32 +2197,32 @@ TACTIC EXTEND ssrabstract
 | [ "abstract" ssrdgens(gens) ] -> [
     if List.length (fst gens) <> 1 then
       errorstrm (str"dependents switches '/' not allowed here");
-    Proofview.V82.tactic (ssrabstract ist gens) ]
+    Ssripats.ssrabstract (ssrdgens_of_parsed_dgens gens) ]
 END
 
 TACTIC EXTEND ssrhave
 | [ "have" ssrhavefwdwbinders(fwd) ] ->
-  [ Proofview.V82.tactic (havetac ist fwd false false) ]
+  [ V82.tactic (havetac ist fwd false false) ]
 END
 
 TACTIC EXTEND ssrhavesuff
 | [ "have" "suff" ssrhpats_nobs(pats) ssrhavefwd(fwd) ] ->
-  [ Proofview.V82.tactic (havetac ist (false,(pats,fwd)) true false) ]
+  [ V82.tactic (havetac ist (false,(pats,fwd)) true false) ]
 END
 
 TACTIC EXTEND ssrhavesuffices
 | [ "have" "suffices" ssrhpats_nobs(pats) ssrhavefwd(fwd) ] ->
-  [ Proofview.V82.tactic (havetac ist (false,(pats,fwd)) true false) ]
+  [ V82.tactic (havetac ist (false,(pats,fwd)) true false) ]
 END
 
 TACTIC EXTEND ssrsuffhave
 | [ "suff" "have" ssrhpats_nobs(pats) ssrhavefwd(fwd) ] ->
-  [ Proofview.V82.tactic (havetac ist (false,(pats,fwd)) true true) ]
+  [ V82.tactic (havetac ist (false,(pats,fwd)) true true) ]
 END
 
 TACTIC EXTEND ssrsufficeshave
 | [ "suffices" "have" ssrhpats_nobs(pats) ssrhavefwd(fwd) ] ->
-  [ Proofview.V82.tactic (havetac ist (false,(pats,fwd)) true true) ]
+  [ V82.tactic (havetac ist (false,(pats,fwd)) true true) ]
 END
 
 (** The "suffice" tactic *)
@@ -2239,7 +2232,7 @@ let pr_ssrsufffwdwbinders _ _ prt (hpats, (fwd, hint)) =
 
 ARGUMENT EXTEND ssrsufffwd
   TYPED AS ssrhpats * (ssrfwd * ssrhint) PRINTED BY pr_ssrsufffwdwbinders
-| [ ssrhpats(pats) ssrbinder_list(bs)  ":" lconstr(t) ssrhint(hint) ] ->
+| [ ssrhpats(pats) ssrbinder_list(bs)  ":" ast_closure_lterm(t) ssrhint(hint) ] ->
   [ let ((clr, pats), binders), simpl = pats in
     let allbs = intro_id_to_binder binders @ bs in
     let allbinders = binders @ List.flatten (binder_to_intro_id bs) in
@@ -2249,11 +2242,11 @@ END
 
 
 TACTIC EXTEND ssrsuff
-| [ "suff" ssrsufffwd(fwd) ] -> [ Proofview.V82.tactic (sufftac ist fwd) ]
+| [ "suff" ssrsufffwd(fwd) ] -> [ V82.tactic (sufftac ist fwd) ]
 END
 
 TACTIC EXTEND ssrsuffices
-| [ "suffices" ssrsufffwd(fwd) ] -> [ Proofview.V82.tactic (sufftac ist fwd) ]
+| [ "suffices" ssrsufffwd(fwd) ] -> [ V82.tactic (sufftac ist fwd) ]
 END
 
 (** The "wlog" (Without Loss Of Generality) tactic *)
@@ -2265,40 +2258,40 @@ let pr_ssrwlogfwd _ _ _ (gens, t) =
 
 ARGUMENT EXTEND ssrwlogfwd TYPED AS ssrwgen list * ssrfwd
                          PRINTED BY pr_ssrwlogfwd
-| [ ":" ssrwgen_list(gens) "/" lconstr(t) ] -> [ gens, mkFwdHint "/" t]
+| [ ":" ssrwgen_list(gens) "/" ast_closure_lterm(t) ] -> [ gens, mkFwdHint "/" t]
 END
 
         
 TACTIC EXTEND ssrwlog
 | [ "wlog" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] ->
-  [ Proofview.V82.tactic (wlogtac ist pats fwd hint false `NoGen) ]
+  [ V82.tactic (wlogtac ist pats fwd hint false `NoGen) ]
 END
 
 TACTIC EXTEND ssrwlogs
 | [ "wlog" "suff" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] ->
-  [ Proofview.V82.tactic (wlogtac ist pats fwd hint true `NoGen) ]
+  [ V82.tactic (wlogtac ist pats fwd hint true `NoGen) ]
 END
 
 TACTIC EXTEND ssrwlogss
 | [ "wlog" "suffices" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ]->
-  [ Proofview.V82.tactic (wlogtac ist pats fwd hint true `NoGen) ]
+  [ V82.tactic (wlogtac ist pats fwd hint true `NoGen) ]
 END
 
 TACTIC EXTEND ssrwithoutloss
 | [ "without" "loss" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] ->
-  [ Proofview.V82.tactic (wlogtac ist pats fwd hint false `NoGen) ]
+  [ V82.tactic (wlogtac ist pats fwd hint false `NoGen) ]
 END
 
 TACTIC EXTEND ssrwithoutlosss
 | [ "without" "loss" "suff" 
     ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] ->
-  [ Proofview.V82.tactic (wlogtac ist pats fwd hint true `NoGen) ]
+  [ V82.tactic (wlogtac ist pats fwd hint true `NoGen) ]
 END
 
 TACTIC EXTEND ssrwithoutlossss
 | [ "without" "loss" "suffices" 
     ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ]->
-  [ Proofview.V82.tactic (wlogtac ist pats fwd hint true `NoGen) ]
+  [ V82.tactic (wlogtac ist pats fwd hint true `NoGen) ]
 END
 
 (* Generally have *)
@@ -2332,14 +2325,14 @@ TACTIC EXTEND ssrgenhave
 | [ "gen" "have" ssrclear(clr)
     ssr_idcomma(id) ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] ->
   [ let pats = augment_preclr clr pats in
-    Proofview.V82.tactic (wlogtac ist pats fwd hint false (`Gen id)) ]
+    V82.tactic (wlogtac ist pats fwd hint false (`Gen id)) ]
 END
 
 TACTIC EXTEND ssrgenhave2
 | [ "generally" "have" ssrclear(clr)
     ssr_idcomma(id) ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] ->
   [ let pats = augment_preclr clr pats in
-    Proofview.V82.tactic (wlogtac ist pats fwd hint false (`Gen id)) ]
+    V82.tactic (wlogtac ist pats fwd hint false (`Gen id)) ]
 END
 
 (* We wipe out all the keywords generated by the grammar rules we defined. *)
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index 4b2fab6d1..4b0bd703a 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -64,12 +64,55 @@ let pr_glob_constr_and_expr = function
 let pr_term (k, c) = pr_guarded (guard_term k) pr_glob_constr_and_expr c
 
 let pr_hyp (SsrHyp (_, id)) = Id.print id
+let pr_hyps = pr_list pr_spc pr_hyp
 
 let pr_occ = function
   | Some (true, occ) -> str "{-" ++ pr_list pr_spc int occ ++ str "}"
   | Some (false, occ) -> str "{+" ++ pr_list pr_spc int occ ++ str "}"
   | 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_dir = function L2R -> str "->" | R2L -> str "<-"
+
+let pr_simpl = function
+  | Simpl -1 -> str "/="
+  | Cut -1 -> str "//"
+  | Simpl n -> str "/" ++ int n ++ str "="
+  | Cut n -> str "/" ++ int n ++ str"/"
+  | SimplCut (-1,-1) -> str "//="
+  | SimplCut (n,-1) -> str "/" ++ int n ++ str "/="
+  | SimplCut (-1,n) -> str "//" ++ int n ++ str "="
+  | SimplCut (n,m) -> str "/" ++ int n ++ str "/" ++ int m ++ str "="
+  | Nop -> mt ()
+
+(* New terms *)
+
+let pr_ast_closure_term { body } = Ppconstr.pr_constr_expr body
+
+let pr_view2 = pr_list mt (fun c -> str "/" ++ pr_ast_closure_term c)
+
+let rec pr_ipat p =
+  match p with
+  | IPatId id -> Id.print id
+  | IPatSimpl sim -> pr_simpl sim
+  | IPatClear clr -> pr_clear mt clr
+  | IPatCase iorpat -> hov 1 (str "[" ++ pr_iorpat iorpat ++ str "]")
+  | IPatDispatch iorpat -> hov 1 (str "/[" ++ pr_iorpat iorpat ++ 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 v -> pr_view2 v
+  | IPatNoop -> str "-"
+  | IPatAbstractVars l -> str "[:" ++ pr_list spc Id.print l ++ str "]"
+  | IPatTac _ -> str "<tac>"
+(* TODO  | IPatAnon Temporary -> str "+" *)
+and pr_ipats ipats = pr_list spc pr_ipat ipats
+and pr_iorpat iorpat = pr_list pr_bar pr_ipats iorpat
+
 (* 0 cost pp function. Active only if Debug Ssreflect is Set *)
 let ppdebug_ref = ref (fun _ -> ())
 let ssr_pp s = Feedback.msg_debug (str"SSR: "++Lazy.force s)
diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli
index f23106826..9fe54e0b1 100644
--- a/plugins/ssr/ssrprinters.mli
+++ b/plugins/ssr/ssrprinters.mli
@@ -27,11 +27,23 @@ val xWithAt : ssrtermkind
 val xNoFlag : ssrtermkind
 val xCpattern : ssrtermkind
 
+val pr_clear : (unit -> Pp.t) -> ssrclear -> Pp.t
+val pr_clear_ne : ssrclear -> Pp.t
+val pr_dir : ssrdir -> Pp.t
+val pr_simpl : ssrsimpl -> Pp.t
+
 val pr_term :
   ssrtermkind * (Glob_term.glob_constr * Constrexpr.constr_expr option) ->
   Pp.t
 
+val pr_ast_closure_term : ast_closure_term -> Pp.t
+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_hyp : ssrhyp -> Pp.t
+val pr_hyps : ssrhyps -> Pp.t
 
 val prl_constr_expr : Constrexpr.constr_expr -> Pp.t
 val prl_glob_constr : Glob_term.glob_constr -> Pp.t
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 6514b186e..63d79198e 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -45,7 +45,7 @@ let rot_hyps dir i hyps =
 
 let tclSEQAT ist atac1 dir (ivar, ((_, atacs2), atac3)) =
   let i = get_index ivar in
-  let evtac = ssrevaltac ist in
+  let evtac t = Proofview.V82.of_tactic (ssrevaltac ist t) in
   let tac1 = evtac atac1 in
   if atacs2 = [] && atac3 <> None then tclPERM (rot_hyps dir i) tac1  else
   let evotac = function Some atac -> evtac atac | _ -> Tacticals.tclIDTAC in
@@ -91,10 +91,11 @@ let hidetacs clseq idhide cl0 =
 
 let endclausestac id_map clseq gl_id cl0 gl =
   let not_hyp' id = not (List.mem_assoc id id_map) in
-  let orig_id id = try List.assoc id id_map with _ -> id in
+  let orig_id id = try List.assoc id id_map with Not_found -> id in
   let dc, c = EConstr.decompose_prod_assum (project gl) (pf_concl gl) in
   let hide_goal = hidden_clseq clseq in
-  let c_hidden = hide_goal && EConstr.eq_constr (project gl) c (EConstr.mkVar gl_id) in
+  let c_hidden =
+    hide_goal && EConstr.eq_constr (project gl) c (EConstr.mkVar gl_id) in
   let rec fits forced = function
   | (id, _) :: ids, decl :: dc' when RelDecl.get_name decl = Name id ->
     fits true (ids, dc')
@@ -114,26 +115,28 @@ let endclausestac id_map clseq gl_id cl0 gl =
   let ugtac gl' =
     Proofview.V82.of_tactic
       (convert_concl_no_check (unmark (pf_concl gl'))) gl' in
-  let ctacs = if hide_goal then [Proofview.V82.of_tactic (Tactics.clear [gl_id])] else [] in
+  let ctacs =
+    if hide_goal then [Proofview.V82.of_tactic (Tactics.clear [gl_id])]
+    else [] in
   let mktac itacs = Tacticals.tclTHENLIST (itacs @ utacs @ ugtac :: ctacs) in
   let itac (_, id) = Proofview.V82.of_tactic (Tactics.introduction id) in
   if fits false (id_map, List.rev dc) then mktac (List.map itac id_map) gl else
   let all_ids = ids_of_rel_context dc @ pf_ids_of_hyps gl in
   if List.for_all not_hyp' all_ids && not c_hidden then mktac [] gl else
-  CErrors.user_err (Pp.str "tampering with discharged assumptions of \"in\" tactical")
+  errorstrm Pp.(str "tampering with discharged assumptions of \"in\" tactical")
 
 let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs)
 
-let tclCLAUSES ist tac (gens, clseq) gl =
+let tclCLAUSES tac (gens, clseq) gl =
   if clseq = InGoal || clseq = InSeqGoal then tac gl else
   let clr_gens = pf_clauseids gl gens clseq in
   let clear = Tacticals.tclTHENLIST (List.rev(List.fold_right clr_of_wgen clr_gens [])) in
-  let gl_id = mk_anon_id hidden_goal_tag gl in
+  let gl_id = mk_anon_id hidden_goal_tag (Tacmach.pf_ids_of_hyps gl) in
   let cl0 = pf_concl gl in
   let dtac gl =
     let c = pf_concl gl in
     let gl, args, c =
-      List.fold_right (abs_wgen true ist mk_discharged_id) gens (gl,[], c) in
+      List.fold_right (abs_wgen true mk_discharged_id) gens (gl,[], c) in
     apply_type c args gl in
   let endtac =
     let id_map = CList.map_filter (function
@@ -147,7 +150,7 @@ let tclCLAUSES ist tac (gens, clseq) gl =
 let hinttac ist is_by (is_or, atacs) =
   let dtac = if is_by then donetac ~-1 else Tacticals.tclIDTAC in
   let mktac = function
-  | Some atac -> Tacticals.tclTHEN (ssrevaltac ist atac) dtac
+  | Some atac -> Tacticals.tclTHEN (Proofview.V82.of_tactic (ssrevaltac ist atac)) dtac
   | _ -> dtac in
   match List.map mktac atacs with
   | [] -> if is_or then dtac else Tacticals.tclIDTAC
@@ -156,4 +159,7 @@ let hinttac ist is_by (is_or, atacs) =
 
 let ssrdotac ist (((n, m), tac), clauses) =
   let mul = get_index n, m in
-  tclCLAUSES ist (tclMULT mul (hinttac ist false tac)) clauses
+  tclCLAUSES (tclMULT mul (hinttac ist false tac)) clauses
+
+let tclCLAUSES tac g_c =
+  Proofview.V82.(tactic (tclCLAUSES (of_tactic tac) g_c))
diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli
index c1f65a31e..5913c09d4 100644
--- a/plugins/ssr/ssrtacticals.mli
+++ b/plugins/ssr/ssrtacticals.mli
@@ -19,14 +19,13 @@ val tclSEQAT :
   Tacmach.tactic
 
 val tclCLAUSES :
-  Ltac_plugin.Tacinterp.interp_sign ->
-  Proofview.V82.tac ->
+  unit Proofview.tactic ->
   (Ssrast.ssrhyps *
      ((Ssrast.ssrhyp_or_id * string) *
         Ssrmatching_plugin.Ssrmatching.cpattern option)
        option)
     list * Ssrast.ssrclseq ->
-  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
+  unit Proofview.tactic
 
 val hinttac :
            Tacinterp.interp_sign ->
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 96ded5abf..2dfcb8572 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -501,21 +501,19 @@ END
 (* View purpose *)
 
 let pr_viewpos = function
-  | 0 -> str " for move/"
-  | 1 -> str " for apply/"
-  | 2 -> str " for apply//"
-  | _ -> mt ()
+  | Some Ssrview.AdaptorDb.Forward -> str " for move/"
+  | Some Ssrview.AdaptorDb.Backward -> str " for apply/"
+  | Some Ssrview.AdaptorDb.Equivalence -> str " for apply//"
+  | None -> mt ()
 
 let pr_ssrviewpos _ _ _ = pr_viewpos
 
-let mapviewpos f n k = if n < 3 then f n else for i = 0 to k - 1 do f i done
-
-ARGUMENT EXTEND ssrviewpos TYPED AS int PRINTED BY pr_ssrviewpos
-  | [ "for" "move" "/" ] -> [ 0 ]
-  | [ "for" "apply" "/" ] -> [ 1 ]
-  | [ "for" "apply" "/" "/" ] -> [ 2 ]
-  | [ "for" "apply" "//" ] -> [ 2 ]
-  | [ ] -> [ 3 ]
+ARGUMENT EXTEND ssrviewpos PRINTED BY pr_ssrviewpos
+  | [ "for" "move" "/" ] -> [ Some Ssrview.AdaptorDb.Forward ]
+  | [ "for" "apply" "/" ] -> [ Some Ssrview.AdaptorDb.Backward ]
+  | [ "for" "apply" "/" "/" ] -> [ Some Ssrview.AdaptorDb.Equivalence ]
+  | [ "for" "apply" "//" ] -> [ Some Ssrview.AdaptorDb.Equivalence ]
+  | [ ] -> [ None ]
 END
 
 let pr_ssrviewposspc _ _ _ i = pr_viewpos i ++ spc ()
@@ -524,19 +522,35 @@ ARGUMENT EXTEND ssrviewposspc TYPED AS ssrviewpos PRINTED BY pr_ssrviewposspc
   | [ ssrviewpos(i) ] -> [ i ]
 END
 
-let print_view_hints i =
-  let pp_viewname = str "Hint View" ++ pr_viewpos i ++ str " " in
-  let pp_hints = pr_list spc pr_rawhintref Ssrview.viewtab.(i) in
+let print_view_hints kind l =
+  let pp_viewname = str "Hint View" ++ pr_viewpos (Some kind) ++ str " " in
+  let pp_hints = pr_list spc pr_rawhintref l in
   Feedback.msg_info  (pp_viewname ++ hov 0 pp_hints ++ Pp.cut ())
 
 VERNAC COMMAND EXTEND PrintView CLASSIFIED AS QUERY
-| [ "Print" "Hint" "View" ssrviewpos(i) ] -> [ mapviewpos print_view_hints i 3 ]
+| [ "Print" "Hint" "View" ssrviewpos(i) ] ->
+  [ match i with
+    | Some k -> print_view_hints k (Ssrview.AdaptorDb.get k)
+    | None ->
+        List.iter (fun k -> print_view_hints k (Ssrview.AdaptorDb.get k))
+          [ Ssrview.AdaptorDb.Forward;
+            Ssrview.AdaptorDb.Backward;
+            Ssrview.AdaptorDb.Equivalence ]
+  ]
 END
 
+let glob_view_hints lvh =
+  List.map (Constrintern.intern_constr (Global.env ()) (Evd.from_env (Global.env ()))) lvh
 
 VERNAC COMMAND EXTEND HintView CLASSIFIED AS SIDEFF
   |  [ "Hint" "View" ssrviewposspc(n) ne_ssrhintref_list(lvh) ] ->
-     [ mapviewpos (Ssrview.add_view_hints (Ssrview.glob_view_hints lvh)) n 2 ]
+     [ let hints = glob_view_hints lvh in
+       match n with
+       | None ->
+          Ssrview.AdaptorDb.declare Ssrview.AdaptorDb.Forward hints;
+          Ssrview.AdaptorDb.declare Ssrview.AdaptorDb.Backward hints
+       | Some k ->
+          Ssrview.AdaptorDb.declare k hints ]
 END
 
 (* }}} *)
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index f2990070b..cb67f538e 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -6,121 +6,325 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-
 open Util
 open Names
-open Term
+
 open Ltac_plugin
-open Tacinterp
-open Glob_term
-open Tacmach
-open Tacticals
+
+open Proofview
+open Notations
 
 open Ssrcommon
+open Ssrast
+
+module AdaptorDb = struct
+
+  type kind = Forward | Backward | Equivalence
+
+  module AdaptorKind = struct
+    type t = kind
+    let compare = Pervasives.compare
+  end
+  module AdaptorMap = Map.Make(AdaptorKind)
+
+  let term_view_adaptor_db =
+    Summary.ref ~name:"view_adaptor_db" AdaptorMap.empty
+
+  let get k =
+    try AdaptorMap.find k !term_view_adaptor_db
+    with Not_found -> []
+
+  let cache_adaptor (_, (k, t)) =
+    let lk = get k in
+    if not (List.exists (Glob_ops.glob_constr_eq t) lk) then
+      term_view_adaptor_db := AdaptorMap.add k (t :: lk) !term_view_adaptor_db
+
+  let subst_adaptor ( subst, (k, t as a)) =
+    let t' = Detyping.subst_glob_constr subst t in
+    if t' == t then a else k, t'
+
+  let classify_adaptor x = Libobject.Substitute x
+
+  let in_db =
+    Libobject.declare_object {
+       (Libobject.default_object "VIEW_ADAPTOR_DB")
+    with
+       Libobject.open_function = (fun i o -> if i = 1 then cache_adaptor o);
+       Libobject.cache_function = cache_adaptor;
+       Libobject.subst_function = subst_adaptor;
+       Libobject.classify_function = classify_adaptor }
+
+  let declare kind terms =
+    List.iter (fun term -> Lib.add_anonymous_leaf (in_db (kind,term)))
+      (List.rev terms)
+
+end
+
+(* Forward View application code *****************************************)
+
+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 vsASSERT_EMPTY : unit tactic
+
+end = struct (* {{{ *)
+
+type vstate = {
+  subject_name : Id.t option;   (* top *)
+    (* None if views are being applied to a term *)
+  view : EConstr.t;  (* v2 (v1 top) *)
+}
+
+include Ssrcommon.MakeState(struct
+  type state = vstate option
+  let init = None
+end)
 
-(* The table and its display command *)
-
-(* FIXME this looks hackish *)
-
-let viewtab : glob_constr list array = Array.make 3 []
-
-let _ =
-  let init () = Array.fill viewtab 0 3 [] in
-  let freeze _ = Array.copy viewtab in
-  let unfreeze vt = Array.blit vt 0 viewtab 0 3 in
-  Summary.declare_summary "ssrview"
-    { Summary.freeze_function   = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function     = init }
-
-(* Populating the table *)
-
-let cache_viewhint (_, (i, lvh)) =
-  let mem_raw h = List.exists (Glob_ops.glob_constr_eq h) in
-  let add_hint h hdb = if mem_raw h hdb then hdb else h :: hdb in
-  viewtab.(i) <- List.fold_right add_hint lvh viewtab.(i)
-
-let subst_viewhint ( subst, (i, lvh as ilvh)) =
-  let lvh' = List.smartmap (Detyping.subst_glob_constr subst) lvh in
-  if lvh' == lvh then ilvh else i, lvh'
-      
-let classify_viewhint x = Libobject.Substitute x
-
-let in_viewhint =
-  Libobject.declare_object {(Libobject.default_object "VIEW_HINTS") with
-       Libobject.open_function = (fun i o -> if i = 1 then cache_viewhint o);
-       Libobject.cache_function = cache_viewhint;
-       Libobject.subst_function = subst_viewhint;
-       Libobject.classify_function = classify_viewhint }
-
-let glob_view_hints lvh =
-  let env = Global.env () in
-  List.map (Constrintern.intern_constr env Evd.(from_env env)) lvh
-
-let add_view_hints lvh i = Lib.add_anonymous_leaf (in_viewhint (i, lvh))
-
-let interp_view ist si env sigma gv rv rid =
-  match DAst.get rv with
-  | GApp (h, rargs) when (match DAst.get h with GHole _ -> true | _ -> false) ->
-    let loc = rv.CAst.loc in
-    let rv = DAst.make ?loc @@ GApp (rid, rargs) in
-    snd (interp_open_constr ist (re_sig si sigma) (rv, None))
+let vsINIT view = tclSET (Some { subject_name = None; view })
+
+let vsPUSH k =
+  tacUPDATE (fun s -> match s with
+  | Some { subject_name; view } ->
+      k view >>= fun view ->
+      tclUNIT (Some { subject_name; view })
+  | None ->
+      Goal.enter_one ~__LOC__ begin fun gl ->
+        let concl = Goal.concl gl in
+        let id = (* We keep the orig name for checks in "in" tcl *)
+          match EConstr.kind_of_type (Goal.sigma gl) concl with
+          | Term.ProdType(Name.Name id, _, _)
+            when Ssrcommon.is_discharged_id id -> id
+          | _ -> 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 })
+      end)
+
+let vsCONSUME k =
+  tclGET (fun s -> match s with
+  | Some { subject_name; view } ->
+        tclSET None <*>
+        k subject_name view
+  | None -> anomaly "vsCONSUME: empty storage")
+
+let vsASSERT_EMPTY =
+  tclGET (function
+  | Some _ -> anomaly ("vsASSERT_EMPTY: not empty")
+  | _ -> tclUNIT ())
+
+end (* }}} *)
+
+let intern_constr_expr { Genintern.genv; ltacvars = vars } sigma ce =
+  let ltacvars = {
+    Constrintern.empty_ltac_sign with Constrintern.ltac_vars = vars } in
+  Constrintern.intern_gen Pretyping.WithoutTypeConstraint ~ltacvars genv sigma ce
+
+(* Disambiguation of /t
+    - t is ltac:(tactic args)
+    - t is a term
+   To allow for t being a notation, like "Notation foo x := ltac:(foo x)", we
+   need to internalize t.
+*)
+let is_tac_in_term { body; glob_env; interp_env } =
+  Goal.(enter_one ~__LOC__ begin fun goal ->
+    let genv = env goal in
+    let sigma = sigma goal in
+    let ist = Ssrcommon.option_assert_get glob_env (Pp.str"not a term") in
+    (* We use the env of the goal, not the global one *)
+    let ist = { ist with Genintern.genv } in
+    (* We unravel notations *)
+    let g = intern_constr_expr ist sigma body in
+    match DAst.get g with
+    | 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))
+end)
+
+(* To inject a constr into a glob_constr we use an Ltac variable *)
+let tclINJ_CONSTR_IST ist p =
+  let fresh_id = Ssrcommon.mk_internal_id "ssr_inj_constr_in_glob" in
+  let ist = {
+    ist with Geninterp.lfun =
+      Id.Map.add fresh_id (Taccoerce.Value.of_constr p) ist.Geninterp.lfun} in
+  tclUNIT (ist,Glob_term.GVar fresh_id)
+
+let mkGHole =
+  DAst.make
+    (Glob_term.GHole(Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None))
+let rec mkGHoles n = if n > 0 then mkGHole :: mkGHoles (n - 1) else []
+let mkGApp f args =
+  if args = [] then f
+  else DAst.make (Glob_term.GApp (f, args))
+
+(* From glob_constr to open_constr === (env,sigma,constr) *)
+let interp_glob ist glob = Goal.enter_one ~__LOC__ begin fun goal ->
+  let env = Goal.env goal in
+  let sigma = Goal.sigma goal in
+  Ssrprinters.ppdebug (lazy
+    Pp.(str"interp-in: " ++ Printer.pr_glob_constr_env env glob));
+  try
+    let sigma,term = Tacinterp.interp_open_constr ist env sigma (glob,None) in
+    Ssrprinters.ppdebug (lazy
+      Pp.(str"interp-out: " ++ Printer.pr_econstr_env env sigma term));
+    tclUNIT (env,sigma,term)
+  with e ->
+    Ssrprinters.ppdebug (lazy
+    Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env glob));
+     tclZERO e
+end
+
+(* Commits the term to the monad *)
+(* I think we should make the API safe by storing here the original evar map,
+ * so that one cannot commit it wrongly.
+ * We could also commit the term automatically, but this makes the code less
+ * modular, see the 2 functions below that would need to "uncommit" *)
+let tclKeepOpenConstr (_env, sigma, t) = Unsafe.tclEVARS sigma <*> tclUNIT t
+
+(* 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         *)
+(* typecheck the partial application, so we use a minimum of 5. *)
+(* Also, we don't handle delayed or iterated coercions to       *)
+(* FUNCLASS, which is probably just as well since these can     *)
+(* lead to infinite arities.                                    *)
+let guess_max_implicits ist glob =
+  Proofview.tclORELSE
+    (interp_glob ist (mkGApp glob (mkGHoles 6)) >>= fun (env,sigma,term) ->
+     let term_ty = Retyping.get_type_of env sigma term in
+     let ctx, _ = Reductionops.splay_prod env sigma term_ty in
+     tclUNIT (List.length ctx + 6))
+  (fun _ -> tclUNIT 5)
+
+let pad_to_inductive ist glob = Goal.enter_one ~__LOC__ begin fun goal ->
+  interp_glob ist glob >>= fun (env, sigma, term) ->
+  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")
+end
+
+(* There are two ways of "applying" a view to term:            *)
+(*  1- using a view hint if the view is an instance of some    *)
+(*     (reflection) inductive predicate.                       *)
+(*  2- applying the view if it coerces to a function, adding   *)
+(*     implicit arguments.                                     *)
+(* 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 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 *)
+  tclINJ_CONSTR_IST ist p >>= fun (ist, p_id) ->
+  let p_id = DAst.make p_id in
+  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
   | _ ->
-  let interp rc rargs =
-    interp_open_constr ist (re_sig si sigma) (mkRApp rc rargs, None) in
-  let rec simple_view rargs n =
-    if n < 0 then view_error "use" gv else
-    try interp rv rargs with _ -> simple_view (mkRHole :: rargs) (n - 1) in
-  let view_nbimps = interp_view_nbimps ist (re_sig si sigma) rv in
-  let view_args = [mkRApp rv (mkRHoles view_nbimps); rid] in
-  let rec view_with = function
-  | [] -> simple_view [rid] (interp_nbargs ist (re_sig si sigma) rv)
-  | hint :: hints -> try interp hint view_args with _ -> view_with hints in
-  snd (view_with (if view_nbimps < 0 then [] else viewtab.(0)))
-
-
-let with_view ist ~next si env (gl0 : (Goal.goal * tac_ctx) Evd.sigma) c name cl prune (conclude : EConstr.t -> EConstr.t -> tac_ctx tac_a) clr =
-  let c2r ist x = { ist with lfun =
-    Id.Map.add top_id (Value.of_constr x) ist.lfun } in
-  let terminate (sigma, c') =
-    let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in
-    let c' = Reductionops.nf_evar sigma c' in
-    let n, c', _, ucst = without_ctx pf_abs_evars gl0 (sigma, c') in
-    let c' = if not prune then c' else without_ctx pf_abs_cterm gl0 n c' in
-    let gl0 = pf_merge_uc ucst gl0 in
-    let gl0, ap =
-      let gl0, ctx = pull_ctx gl0 in
-      let gl0, ap = pf_abs_prod name gl0 c' (Termops.prod_applist sigma cl [c]) in
-      push_ctx ctx gl0, ap in
-    let gl0 = pf_merge_uc_of sigma gl0 in
-    ap, c', gl0 in
-  let rec loop (sigma, c') = function
-  | [] ->
-      let ap, c', gl = terminate (sigma, c') in
-      ap, c', conclude ap c' gl
-  | f :: view ->
-      let ist, rid =
-        match EConstr.kind sigma c' with
-        | Var id -> ist,mkRVar id
-        | _ -> c2r ist c',mkRltacVar top_id in
-      let v = intern_term ist env f in
-      loop (interp_view ist si env sigma f v rid) view
-  in loop
-
-let pfa_with_view ist ?(next=ref []) (prune, view) cl c conclude clr gl =
-  let env, sigma, si =
-    without_ctx pf_env gl, Refiner.project gl, without_ctx sig_it gl in
-  with_view
-    ist ~next si env gl c (constr_name sigma c) cl prune conclude clr (sigma, c) view 
-
-let pf_with_view_linear ist gl v cl c =
-  let x,y,gl =
-    pfa_with_view ist v cl c (fun _ _ -> tac_ctx tclIDTAC) []
-      (push_ctx (new_ctx ()) gl) in
-  let gl, _ = pull_ctxs gl in
-  assert(List.length (sig_it gl) = 1);
-  x,y,re_sig (List.hd (sig_it gl)) (Refiner.project gl)
+     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 ->
+        Ssrcommon.tclFIRSTa (List.map
+          (fun a -> interp_glob ist (mkGApp a [vpad; p_id])) adaptors))
+       (fun _ ->
+        guess_max_implicits ist v >>= fun n ->
+        Ssrcommon.tclFIRSTi (fun n ->
+           interp_glob ist (mkGApp v (mkGHoles n @ [p_id]))) n)
+     >>= tclKeepOpenConstr
+
+(* we store in the state (v top), then (v1 (v2 top))... *)
+let pile_up_view (ist, v) =
+  let ist = Ssrcommon.option_assert_get ist (Pp.str"not a term") in
+  State.vsPUSH (fun p -> interp_view ist v p)
+
+let finalize_view s0 ?(simple_types=true) p =
+Goal.enter_one ~__LOC__ begin fun g ->
+  let env = Goal.env g in
+  let sigma = Goal.sigma g in
+  let evars_of_p = Evd.evars_of_term (EConstr.to_constr sigma p) in
+  let filter x _ = Evar.Set.mem x evars_of_p in
+  let sigma = Typeclasses.resolve_typeclasses ~fail:false ~filter env sigma in
+  let p = Reductionops.nf_evar sigma p in
+  let get_body = function Evd.Evar_defined x -> x | _ -> assert false in
+  let evars_of_econstr sigma t =
+    Evd.evars_of_term (EConstr.to_constr sigma (EConstr.of_constr t)) in
+  let rigid_of s =
+    List.fold_left (fun l k ->
+      if Evd.is_defined sigma k then
+        let bo = get_body Evd.(evar_body (find sigma k)) in
+          k :: l @ Evar.Set.elements (evars_of_econstr sigma bo)
+      else l
+    ) [] s in
+  let und0 = (* Unassigned evars in the initial goal *)
+    let sigma0 = Tacmach.project s0 in
+    let g0info = Evd.find sigma0 (Tacmach.sig_it s0) in
+    let g0 = Evd.evars_of_filtered_evar_info g0info in
+    List.filter (fun k -> Evar.Set.mem k g0)
+      (List.map fst (Evar.Map.bindings (Evd.undefined_map sigma0))) in
+  let rigid = rigid_of und0 in
+  let n, p, to_prune, _ucst = pf_abs_evars2 s0 rigid (sigma, p) in
+  let p = if simple_types then pf_abs_cterm s0 n p else p in
+  Ssrprinters.ppdebug (lazy Pp.(str"view@finalized: " ++
+    Printer.pr_econstr_env env sigma p));
+  let sigma = List.fold_left Evd.remove sigma to_prune in
+  Unsafe.tclEVARS sigma <*>
+  tclUNIT p
+end
+
+let pose_proof subject_name p =
+  Tactics.generalize [p] <*>
+  Option.cata
+    (fun id -> Ssrcommon.tclRENAME_HD_PROD (Name.Name id)) (tclUNIT())
+    subject_name
+  <*>
+  Tactics.New.reduce_after_refine
+
+let rec apply_all_views ending vs s0 =
+  match vs with
+  | [] -> ending s0
+  | v :: vs ->
+      Ssrprinters.ppdebug (lazy Pp.(str"piling..."));
+      is_tac_in_term v >>= function
+      | `Tac tac ->
+           Ssrprinters.ppdebug (lazy Pp.(str"..a tactic"));
+           ending s0 <*> Tacinterp.eval_tactic tac <*>
+           Ssrcommon.tacSIGMA >>= apply_all_views ending vs
+      | `Term v ->
+           Ssrprinters.ppdebug (lazy Pp.(str"..a term"));
+           pile_up_view v <*> apply_all_views ending vs s0
+
+(* Entry points *********************************************************)
+
+let tclIPAT_VIEWS ~views:vs ~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
+  tclINDEPENDENT begin
+    State.vsASSERT_EMPTY <*>
+    Ssrcommon.tacSIGMA >>= apply_all_views 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
+  tclINDEPENDENT begin
+    State.vsASSERT_EMPTY <*>
+    State.vsINIT subject <*>
+    Ssrcommon.tacSIGMA >>= apply_all_views ending_tac vs <*>
+    State.vsASSERT_EMPTY
+  end
 
 (* vim: set filetype=ocaml foldmethod=marker: *)
diff --git a/plugins/ssr/ssrview.mli b/plugins/ssr/ssrview.mli
index 6fd906ff4..986b5fbf5 100644
--- a/plugins/ssr/ssrview.mli
+++ b/plugins/ssr/ssrview.mli
@@ -6,31 +6,32 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-
 open Ssrast
-open Ssrcommon
 
-val viewtab : Glob_term.glob_constr list array
-val add_view_hints : Glob_term.glob_constr list -> int -> unit
-val glob_view_hints : Constrexpr.constr_expr list -> Glob_term.glob_constr list
+(* Adaptor DB (Hint View) *)
+module AdaptorDb : sig
+
+  type kind = Forward | Backward | Equivalence
 
-val pfa_with_view :
-           ist ->
-           ?next:ssripats ref ->
-           bool * ssrterm list ->
-           EConstr.t ->
-           EConstr.t ->
-           (EConstr.t -> EConstr.t -> tac_ctx tac_a) ->
-           ssrhyps ->
-   (goal * tac_ctx) sigma -> EConstr.types * EConstr.t * (goal * tac_ctx) list sigma
+  val get : kind -> Glob_term.glob_constr list
+  val declare : kind -> Glob_term.glob_constr list -> unit
 
-val pf_with_view_linear :
-           ist ->
-           goal sigma ->
-           bool * ssrterm list ->
-           EConstr.t ->
-           EConstr.t ->
-           EConstr.types * EConstr.t * goal sigma
+end
 
+(* Apply views to the top of the stack (intro pattern) *)
+val tclIPAT_VIEWS :
+    views:ast_closure_term list ->
+    conclusion:(to_clear:Names.Id.t list -> unit Proofview.tactic) ->
+  unit Proofview.tactic
 
+(* Apply views to a given subject (as if was the top of the stack), then
+   call conclusion on the obtained term (something like [v2 (v1 subject)]).
+   The term being passed to conclusion is abstracted over non-resolved evars:
+   if [simple_types] then all unnecessary dependencies among the abstracted
+   evars are pruned *)
+val tclWITH_FWD_VIEWS :
+  simple_types:bool ->
+    subject:EConstr.t ->
+    views:ast_closure_term list ->
+    conclusion:(EConstr.t -> unit Proofview.tactic) ->
+  unit Proofview.tactic