ssr: rewrite Ssripats and Ssrview in the tactic monad

Ssripats and Ssrview are now written in the Tactic Monad.
Ssripats implements the => tactical.
Ssrview implements the application of forward views.

The code is, according to my tests, 100% backward compatible.
The code is much more documented than before.
Moreover the "ist" (ltac context) used to interpret views is the correct
one (the one at ARGUMENT EXTEND interp time, not the one at TACTIC
EXTEND execution time).  Some of the code not touched by this commit
still uses the incorrect ist, so its visibility in TACTIC EXTEND
can't be removed yet.

The main changes in the code are:
- intro patterns are implemented using a state machine (a goal comes
  with a state). Ssrcommon.MakeState provides an easy way for a tactic
  to enrich the goal with with data of interest, such as the set of
  hyps to be cleared.  This cleans up the old implementation that, in
  order to thread the state, that to redefine a bunch of tclSTUFF
- the interpretation of (multiple) forward views uses the state to
  accumulate intermediate results
- the bottom of Sscommon collects a bunch of utilities written in the
  tactic monad. Most of them are the rewriting of already existing
  utilities.  When possible the old version was removed.

1 files changed, 226 insertions, 233 deletions

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. *)