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, 662 insertions, 361 deletions

diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index b3be31b7b..77ebe17a4 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 (Ssrelim.perform_injection t)
+    else
+      Ssrelim.ssrscasetac false 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 (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 (Ssrequality.simpltac (Simpl n))
+  | IPatSimpl (Cut n) ->
+       V82.tactic (Ssrequality.simpltac (Cut n))
+  | IPatSimpl (SimplCut (n,m)) ->
+       V82.tactic (Ssrequality.simpltac (SimplCut (n,m)))
+
+  | IPatRewrite (occ,dir) ->
+     Ssrcommon.tclWITHTOP
+       (fun x -> V82.tactic (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 (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 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 Ssrcommon.unprotecttac else tclUNIT () in
+  V82.of_tactic begin
+    V82.tactic 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
+          (Ssrelim.ssrelim deps (`EGen gen) ~elim eqid (elim_intro_tac ipats)))
+        cs)
+    | [] ->
+      tclINDEPENDENT
+        (V82.tactic
+          (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 (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
+            (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.ssrscasetac false)
+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 (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 (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: *)