Merge branch 'trunk' into located_switch

28 files changed, 227 insertions, 190 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 74cb7a364..c2d12ebd0 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -10,16 +10,12 @@ module CVars = Vars
 
 open Pp
 open Util
-open CErrors
 open Names
-open Vars
 open Termops
 open EConstr
 open Environ
-open Tacmach
 open Genredexpr
 open Tactics
-open Tacticals
 open Clenv
 open Locus
 open Proofview.Notations
@@ -380,7 +376,7 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
 and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) =
   let tactic = function
     | Res_pf (c,cl) -> unify_resolve_gen poly flags (c,cl)
-    | ERes_pf _ -> Proofview.V82.tactic (fun gl -> error "eres_pf")
+    | ERes_pf _ -> Proofview.Goal.enter { enter = fun gl -> Tacticals.New.tclZEROMSG (str "eres_pf") }
     | Give_exact (c, cl)  -> exact poly (c, cl)
     | Res_pf_THEN_trivial_fail (c,cl) ->
       Tacticals.New.tclTHEN
@@ -389,10 +385,11 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=
 	   with "debug auto" we don't display the details of inner trivial *)
         (trivial_fail_db (no_dbg ()) (not (Option.is_empty flags)) db_list local_db)
     | Unfold_nth c ->
-      Proofview.V82.tactic (fun gl ->
-       if exists_evaluable_reference (pf_env gl) c then
-	 tclPROGRESS (Proofview.V82.of_tactic (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)) gl
-       else tclFAIL 0 (str"Unbound reference") gl)
+      Proofview.Goal.enter { enter = begin fun gl ->
+       if exists_evaluable_reference (Tacmach.New.pf_env gl) c then
+	 Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)
+       else Tacticals.New.tclFAIL 0 (str"Unbound reference")
+       end }
     | Extern tacast -> 
       conclPattern concl p tacast
   in
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 32710e347..9ed9f0ae2 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -9,7 +9,6 @@
 (** This files implements auto and related automation tactics *)
 
 open Names
-open Term
 open EConstr
 open Clenv
 open Pattern
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index ff8b54ebf..68f72d7ae 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -9,8 +9,6 @@
 open Equality
 open Names
 open Pp
-open Tacticals
-open Tactics
 open Term
 open Termops
 open CErrors
@@ -127,45 +125,13 @@ let autorewrite ?(conds=Naive) tac_main lbas =
       (Proofview.tclUNIT()) lbas))
 
 let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
  (* let's check at once if id exists (to raise the appropriate error) *)
- let _ = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) idl in
- let general_rewrite_in id =
-  let id = ref id in
-  let to_be_cleared = ref false in
-   fun dir cstr tac gl ->
-    let last_hyp_id =
-     match Tacmach.pf_hyps gl with
-        d :: _ -> Context.Named.Declaration.get_id d
-      | _ -> (* even the hypothesis id is missing *)
-        raise (Logic.RefinerError (Logic.NoSuchHyp !id))
-    in
-    let gl' = Proofview.V82.of_tactic (general_rewrite_in dir AllOccurrences true ~tac:(tac, conds) false !id cstr false) gl in
-    let gls = gl'.Evd.it in
-    match gls with
-       g::_ ->
-        (match Environ.named_context_of_val (Goal.V82.hyps gl'.Evd.sigma g) with
-            d ::_ ->
-              let lastid = Context.Named.Declaration.get_id d in
-              if not (Id.equal last_hyp_id lastid) then
-               begin
-                let gl'' =
-                  if !to_be_cleared then
-                   tclTHEN (fun _ -> gl') (tclTRY (Proofview.V82.of_tactic (clear [!id]))) gl
-                  else gl' in
-                id := lastid ;
-                to_be_cleared := true ;
-                gl''
-               end
-              else
-               begin
-                to_be_cleared := false ;
-                gl'
-               end
-          | _ -> assert false) (* there must be at least an hypothesis *)
-     | _ -> assert false (* rewriting cannot complete a proof *)
- in
- let general_rewrite_in x y z w = Proofview.V82.tactic (general_rewrite_in x y (EConstr.of_constr z) w) in
+  let _ = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) idl in
+  let general_rewrite_in id dir cstr tac =
+    let cstr = EConstr.of_constr cstr in
+    general_rewrite_in dir AllOccurrences true ~tac:(tac, conds) false id cstr false
+  in
  Tacticals.New.tclMAP (fun id ->
   Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS
     (List.fold_left (fun tac bas ->
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index 2a5e7c345..27f624f71 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open Pattern
 open Names
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index df222eed8..05eb0a976 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -18,9 +18,7 @@ open Names
 open Term
 open Termops
 open EConstr
-open Reduction
 open Proof_type
-open Tacticals
 open Tacmach
 open Tactics
 open Clenv
@@ -221,18 +219,22 @@ let auto_unif_flags freeze st =
     resolve_evars = false
 }
 
-let e_give_exact flags poly (c,clenv) gl =
+let e_give_exact flags poly (c,clenv) =
+  let open Tacmach.New in
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  let sigma = project gl in
   let (c, _, _) = c in
-  let c, gl =
+  let c, sigma =
     if poly then
       let clenv', subst = Clenv.refresh_undefined_univs clenv in
-      let evd = evars_reset_evd ~with_conv_pbs:true gl.sigma clenv'.evd in
+      let evd = evars_reset_evd ~with_conv_pbs:true sigma clenv'.evd in
       let c = Vars.subst_univs_level_constr subst c in
-        c, {gl with sigma = evd}
-    else c, gl
+        c, evd
+    else c, sigma
   in
-  let t1 = pf_unsafe_type_of gl c in
-  Proofview.V82.of_tactic (Clenvtac.unify ~flags t1 <*> exact_no_check c) gl
+  let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in
+  Sigma.Unsafe.of_pair (Clenvtac.unify ~flags t1 <*> exact_no_check c, sigma)
+  end }
 
 let unify_e_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
   let clenv', c = connect_hint_clenv poly c clenv gls in
@@ -353,12 +355,12 @@ let shelve_dependencies gls =
 
 let hintmap_of sigma hdc secvars concl =
   match hdc with
-  | None -> fun db -> Hint_db.map_none secvars db
+  | None -> fun db -> Hint_db.map_none ~secvars db
   | Some hdc ->
      fun db ->
      if Hint_db.use_dn db then (* Using dnet *)
-       Hint_db.map_eauto sigma secvars hdc concl db
-     else Hint_db.map_existential sigma secvars hdc concl db
+       Hint_db.map_eauto sigma ~secvars hdc concl db
+     else Hint_db.map_existential sigma ~secvars hdc concl db
 
 (** Hack to properly solve dependent evars that are typeclasses *)
 let rec e_trivial_fail_db only_classes db_list local_db secvars =
@@ -455,15 +457,14 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
                    { enter = fun gl -> unify_resolve_refine poly flags gl (c,None,clenv) } in
              Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
-             Proofview.V82.tactic (e_give_exact flags poly (c,clenv))
+             e_give_exact flags poly (c,clenv)
       | Res_pf_THEN_trivial_fail (term,cl) ->
          let fst = with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in
          let snd = if complete then Tacticals.New.tclIDTAC
                    else e_trivial_fail_db only_classes db_list local_db secvars in
          Tacticals.New.tclTHEN fst snd
       | Unfold_nth c ->
-         let tac = Proofview.V82.of_tactic (unfold_in_concl [AllOccurrences,c]) in
-         Proofview.V82.tactic (tclWEAK_PROGRESS tac)
+         Proofview.tclPROGRESS (unfold_in_concl [AllOccurrences,c])
       | Extern tacast -> conclPattern concl p tacast
       in
       let tac = run_hint t tac in
@@ -1201,7 +1202,7 @@ module Search = struct
            Feedback.msg_debug
              (pr_depth info.search_depth ++ str": no match for " ++
                 Printer.pr_econstr_env (Goal.env gl) s concl ++
-                spc () ++ str ", " ++ int (List.length poss) ++
+                str ", " ++ int (List.length poss) ++
                 str" possibilities");
          match e with
          | (ReachedLimitEx,ie) -> Proofview.tclZERO ~info:ie ReachedLimitEx
@@ -1216,7 +1217,6 @@ module Search = struct
 
   let intro_tac info kont gl =
     let open Proofview in
-    let open Proofview.Notations in
     let env = Goal.env gl in
     let sigma = Goal.sigma gl in
     let s = Sigma.to_evar_map sigma in
@@ -1254,7 +1254,6 @@ module Search = struct
   let search_tac_gl ?st only_classes dep hints depth i sigma gls gl :
         unit Proofview.tactic =
     let open Proofview in
-    let open Proofview.Notations in
     if false (* In 8.6, still allow non-class goals only_classes && not (is_class_type sigma (Goal.concl gl)) *) then
       Tacticals.New.tclZEROMSG (str"Not a subgoal for a class")
     else
@@ -1614,9 +1613,11 @@ let not_evar c =
   | Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar")
   | _ -> Proofview.tclUNIT ()
 
-let is_ground c gl =
-  if Evarutil.is_ground_term (project gl) c then tclIDTAC gl
-  else tclFAIL 0 (str"Not ground") gl
+let is_ground c =
+  let open Tacticals.New in
+  Proofview.tclEVARMAP >>= fun sigma ->
+  if Evarutil.is_ground_term sigma c then tclIDTAC
+  else tclFAIL 0 (str"Not ground")
 
 let autoapply c i =
   let open Proofview.Notations in
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index a38be5972..c5731e377 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -9,9 +9,7 @@
 (** This files implements typeclasses eauto *)
 
 open Names
-open Constr
 open EConstr
-open Tacmach
 
 val catchable : exn -> bool
 
@@ -33,7 +31,7 @@ val head_of_constr : Id.t -> constr -> unit Proofview.tactic
 
 val not_evar : constr -> unit Proofview.tactic
 
-val is_ground : constr -> tactic
+val is_ground : constr -> unit Proofview.tactic
 
 val autoapply : constr -> Hints.hint_db_name -> unit Proofview.tactic
 
diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli
index 510b135b0..2cf5a6829 100644
--- a/tactics/contradiction.mli
+++ b/tactics/contradiction.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open EConstr
 open Misctypes
 
diff --git a/tactics/dnet.mli b/tactics/dnet.mli
index 9f29c60b6..565a916f8 100644
--- a/tactics/dnet.mli
+++ b/tactics/dnet.mli
@@ -26,7 +26,7 @@
    distincts, or you'll get unexpected behaviours.
 
    Warning 2: This structure is perfect, i.e. the set of candidates
-   returned is equal to the set of solutions. Beware of DeBruijn
+   returned is equal to the set of solutions. Beware of de Bruijn
    shifts and sorts subtyping though (which makes the comparison not
    symmetric, see term_dnet.ml).
 
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index e2006ac1e..c952f4e72 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -6,9 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open EConstr
-open Proof_type
 open Hints
 open Tactypes
 
diff --git a/tactics/elim.ml b/tactics/elim.ml
index e37ec6bce..855cb206f 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -8,7 +8,6 @@
 
 open Util
 open Names
-open Term
 open Termops
 open EConstr
 open Inductiveops
diff --git a/tactics/elim.mli b/tactics/elim.mli
index dc1af79ba..fb7cc7b83 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open EConstr
 open Tacticals
 open Misctypes
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index bac3980d2..641929a77 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -25,7 +25,6 @@ open Constr_matching
 open Misctypes
 open Tactypes
 open Hipattern
-open Pretyping
 open Proofview.Notations
 open Tacmach.New
 open Coqlib
@@ -67,9 +66,26 @@ let choose_noteq eqonleft =
   else
     left_with_bindings false Misctypes.NoBindings
 
-let mkBranches c1 c2 =
+open Sigma.Notations
+
+(* A surgical generalize which selects the right occurrences by hand *)
+(* This prevents issues where c2 is also a subterm of c1 (see e.g. #5449) *)
+
+let generalize_right mk typ c1 c2 =
+  Proofview.Goal.enter { Proofview.Goal.enter = begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let store = Proofview.Goal.extra gl in
+  Refine.refine ~unsafe:true { Sigma.run = begin fun sigma ->
+    let na = Name (next_name_away_with_default "x" Anonymous (Termops.ids_of_context env)) in
+    let newconcl = mkProd (na, typ, mk typ c1 (mkRel 1)) in
+    let Sigma (x, sigma, p) = Evarutil.new_evar env sigma ~principal:true ~store newconcl in
+    Sigma (mkApp (x, [|c2|]), sigma, p)
+  end }
+  end }
+
+let mkBranches (eqonleft,mk,c1,c2,typ) =
   tclTHENLIST
-    [generalize [c2];
+    [generalize_right mk typ c1 c2;
      Simple.elim c1;
      intros;
      onLastHyp Simple.case;
@@ -145,15 +161,32 @@ let diseqCase hyps eqonleft =
 
 open Proofview.Notations
 
-(* spiwack: a small wrapper around [Hipattern]. *)
+(* spiwack: a PatternMatchingFailure wrapper around [Hipattern]. *)
 
 let match_eqdec sigma c =
-  try Proofview.tclUNIT (match_eqdec sigma c)
+  try
+    let (eqonleft,_,c1,c2,ty) = match_eqdec sigma c in
+    let (op,eq1,noteq,eq2) =
+      match EConstr.kind sigma c with
+      | App (op,[|ty1;ty2|]) ->
+         let ty1, ty2 = if eqonleft then ty1, ty2 else ty2, ty1 in
+         (match EConstr.kind sigma ty1, EConstr.kind sigma ty2 with
+         | App (eq1,_), App (noteq,[|neq|]) ->
+            (match EConstr.kind sigma neq with
+             | App (eq2,_) -> op,eq1,noteq,eq2
+             | _ -> assert false)
+         | _ -> assert false)
+      | _ -> assert false in
+    let mk t x y =
+      let eq = mkApp (eq1,[|t;x;y|]) in
+      let neq = mkApp (noteq,[|mkApp (eq2,[|t;x;y|])|]) in
+      if eqonleft then mkApp (op,[|eq;neq|]) else mkApp (op,[|neq;eq|]) in
+    Proofview.tclUNIT (eqonleft,mk,c1,c2,ty)
   with PatternMatchingFailure -> Proofview.tclZERO PatternMatchingFailure
 
 (* /spiwack *)
 
-let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with
+let rec solveArg hyps eqonleft mk largs rargs = match largs, rargs with
 | [], [] ->
   tclTHENLIST [
     choose_eq eqonleft;
@@ -163,8 +196,8 @@ let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with
 | a1 :: largs, a2 :: rargs ->
   Proofview.Goal.enter { enter = begin fun gl ->
   let rectype = pf_unsafe_type_of gl a1 in
-  let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in
-  let tac hyp = solveArg (hyp :: hyps) eqonleft op largs rargs in
+  let decide = mk rectype a1 a2 in
+  let tac hyp = solveArg (hyp :: hyps) eqonleft mk largs rargs in
   let subtacs =
     if eqonleft then [eqCase tac;diseqCase hyps eqonleft;default_auto]
     else [diseqCase hyps eqonleft;eqCase tac;default_auto] in
@@ -178,13 +211,13 @@ let solveEqBranch rectype =
       Proofview.Goal.enter { enter = begin fun gl ->
         let concl = pf_concl gl in
         let sigma = project gl in
-        match_eqdec sigma concl >>= fun (eqonleft,op,lhs,rhs,_) ->
+        match_eqdec sigma concl >>= fun (eqonleft,mk,lhs,rhs,_) ->
           let (mib,mip) = Global.lookup_inductive rectype in
           let nparams   = mib.mind_nparams in
           let getargs l = List.skipn nparams (snd (decompose_app sigma l)) in
           let rargs   = getargs rhs
           and largs   = getargs lhs in
-          solveArg [] eqonleft op largs rargs
+          solveArg [] eqonleft mk largs rargs
       end }
     end
     begin function (e, info) -> match e with
@@ -204,14 +237,14 @@ let decideGralEquality =
       Proofview.Goal.enter { enter = begin fun gl ->
         let concl = pf_concl gl in
         let sigma = project gl in
-        match_eqdec sigma concl >>= fun (eqonleft,_,c1,c2,typ) ->
+        match_eqdec sigma concl >>= fun (eqonleft,mk,c1,c2,typ as data) ->
         let headtyp = hd_app sigma (pf_compute gl typ) in
         begin match EConstr.kind sigma headtyp with
         | Ind (mi,_) -> Proofview.tclUNIT mi
         | _ -> tclZEROMSG (Pp.str"This decision procedure only works for inductive objects.")
         end >>= fun rectype ->
           (tclTHEN
-             (mkBranches c1 c2)
+             (mkBranches data)
              (tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype)))
       end }
     end
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index b08456f2f..d023b4568 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -105,6 +105,12 @@ let get_coq_eq ctx =
   with Not_found ->
     error "eq not found."
 
+let univ_of_eq env eq =
+  let eq = EConstr.of_constr eq in
+  match kind_of_term (EConstr.Unsafe.to_constr (Retyping.get_type_of env Evd.empty eq)) with
+  | Prod (_,t,_) -> (match kind_of_term t with Sort (Type u) -> u | _ -> assert false)
+  | _ -> assert false
+
 (**********************************************************************)
 (* Check if an inductive type [ind] has the form                      *)
 (*                                                                    *)
@@ -761,7 +767,7 @@ let build_congr env (eq,refl,ctx) ind =
   let ty = RelDecl.get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in
   let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
-  if Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt) then
+  if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then
     error "Constructor must have no arguments";
   let b = List.nth constrargs (i + mib.mind_nparams - 1) in
   let varB = fresh env (Id.of_string "B") in
@@ -769,6 +775,7 @@ let build_congr env (eq,refl,ctx) ind =
   let varf = fresh env (Id.of_string "f") in
   let ci = make_case_info (Global.env()) ind RegularStyle in
   let uni, ctx = Universes.extend_context (Universes.new_global_univ ()) ctx in
+  let ctx = (fst ctx, Univ.enforce_leq uni (univ_of_eq env eq) (snd ctx)) in
   let c = 
   my_it_mkLambda_or_LetIn paramsctxt
      (mkNamedLambda varB (mkSort (Type uni))
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ace7c30e9..b0f27663e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -14,7 +14,6 @@ open Names
 open Nameops
 open Term
 open Termops
-open Environ
 open EConstr
 open Vars
 open Namegen
@@ -97,9 +96,6 @@ let _ =
 
 (* Rewriting tactics *)
 
-let tclNOTSAMEGOAL tac =
-  Proofview.V82.tactic (Tacticals.tclNOTSAMEGOAL (Proofview.V82.of_tactic tac))
-
 type dep_proof_flag = bool (* true = support rewriting dependent proofs *)
 type freeze_evars_flag = bool (* true = don't instantiate existing evars *)
 
@@ -268,6 +264,25 @@ let rewrite_elim with_evars frzevars cls c e =
   general_elim_clause with_evars flags cls c e
   end }
 
+let tclNOTSAMEGOAL tac =
+  let goal gl = Proofview.Goal.goal (Proofview.Goal.assume gl) in
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
+    let sigma = project gl in
+    let ev = goal gl in
+    tac >>= fun () ->
+    Proofview.Goal.goals >>= fun gls ->
+    let check accu gl' =
+      gl' >>= fun gl' ->
+      let accu = accu || Goal.V82.same_goal sigma ev (project gl') (goal gl') in
+      Proofview.tclUNIT accu
+    in
+    Proofview.Monad.List.fold_left check false gls >>= fun has_same ->
+    if has_same then
+      tclZEROMSG (str"Tactic generated a subgoal identical to the original goal.")
+    else
+      Proofview.tclUNIT ()
+  end }
+
 (* Ad hoc asymmetric general_elim_clause *)
 let general_elim_clause with_evars frzevars cls rew elim =
   let open Pretype_errors in
@@ -642,8 +657,8 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
   | Some evd ->
     let e = build_coq_eq () in
     let sym = build_coq_eq_sym () in
-    Tacticals.New.pf_constr_of_global sym (fun sym ->
-    Tacticals.New.pf_constr_of_global e (fun e ->
+    Tacticals.New.pf_constr_of_global sym >>= fun sym ->
+    Tacticals.New.pf_constr_of_global e >>= fun e ->
     let eq = applist (e, [t1;c1;c2]) in
     tclTHENLAST
       (replace_core clause l2r eq)
@@ -651,7 +666,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
          [assumption;
           tclTHEN (apply sym) assumption;
           try_prove_eq
-         ])))
+         ])
   end }
 
 let replace c1 c2 =
@@ -721,7 +736,7 @@ let _ =
       optread  = (fun () -> !keep_proof_equalities_for_injection) ;
       optwrite = (fun b -> keep_proof_equalities_for_injection := b) }
 
-let find_positions env sigma t1 t2 =
+let find_positions env sigma ~no_discr t1 t2 =
   let project env sorts posn t1 t2 =
     let ty1 = get_type_of env sigma t1 in
     let s = get_sort_family_of env sigma ty1 in
@@ -752,7 +767,7 @@ let find_positions env sigma t1 t2 =
             List.flatten
 	      (List.map2_i (fun i -> findrec sorts' ((sp1,adjust i)::posn))
 		0 rargs1 rargs2)
-	  else if Sorts.List.mem InType sorts'
+	  else if Sorts.List.mem InType sorts' && not no_discr
           then (* see build_discriminator *)
 	    raise (DiscrFound (List.rev posn,sp1,sp2))
 	  else 
@@ -776,13 +791,14 @@ let find_positions env sigma t1 t2 =
     Inl (path,c1,c2)
 
 let discriminable env sigma t1 t2 =
-  match find_positions env sigma t1 t2 with
+  match find_positions env sigma ~no_discr:false t1 t2 with
     | Inl _ -> true
     | _ -> false
 
 let injectable env sigma t1 t2 =
-    match find_positions env sigma t1 t2 with
-    | Inl _ | Inr [] | Inr [([],_,_)] -> false
+    match find_positions env sigma ~no_discr:true t1 t2 with
+    | Inl _ -> assert false
+    | Inr [] | Inr [([],_,_)] -> false
     | Inr _ -> true
 
 
@@ -1017,7 +1033,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
   Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
-    match find_positions env sigma t1 t2 with
+    match find_positions env sigma ~no_discr:false t1 t2 with
     | Inr _ ->
 	tclZEROMSG (str"Not a discriminable equality.")
     | Inl (cpath, (_,dirn), _) ->
@@ -1399,9 +1415,9 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
 let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
   let env = eq_clause.env in
-  match find_positions env sigma t1 t2 with
+  match find_positions env sigma ~no_discr:true t1 t2 with
   | Inl _ ->
-     tclZEROMSG (strbrk"This equality is discriminable. You should use the discriminate tactic to solve the goal.")
+     assert false
   | Inr [] ->
      let suggestion =
          if !keep_proof_equalities_for_injection then
@@ -1468,7 +1484,7 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
   Proofview.Goal.enter { enter = begin fun gl ->
     let sigma =  clause.evd in
     let env = Proofview.Goal.env gl in
-      match find_positions env sigma t1 t2 with
+      match find_positions env sigma ~no_discr:false t1 t2 with
       | Inl (cpath, (_,dirn), _) ->
 	  discr_positions env sigma u clause cpath dirn
       | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 5467b4af2..b47be3bbc 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -8,7 +8,6 @@
 
 (*i*)
 open Names
-open Term
 open Evd
 open EConstr
 open Environ
@@ -97,7 +96,10 @@ val cutRewriteInConcl : bool -> constr -> unit Proofview.tactic
 val rewriteInHyp : bool -> constr -> Id.t -> unit Proofview.tactic
 val rewriteInConcl : bool -> constr -> unit Proofview.tactic
 
+(* Tells if tactic "discriminate" is applicable *)
 val discriminable : env -> evar_map -> constr -> constr -> bool
+
+(* Tells if tactic "injection" is applicable *)
 val injectable : env -> evar_map -> constr -> constr -> bool
 
 (* Subst *)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 52e3dd09f..61bc3d284 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-module CVars = Vars
-
 open Pp
 open Util
 open CErrors
@@ -1238,18 +1236,15 @@ let prepare_hint check (poly,local) env init (sigma,c) =
   (* We re-abstract over uninstantiated evars and universes.
      It is actually a bit stupid to generalize over evars since the first
      thing make_resolves will do is to re-instantiate the products *)
-  let sigma, subst = Evd.nf_univ_variables sigma in
+  let sigma, _ = Evd.nf_univ_variables sigma in
   let c = Evarutil.nf_evar sigma c in
-  let c = EConstr.Unsafe.to_constr c in
-  let c = CVars.subst_univs_constr subst c in
-  let c = EConstr.of_constr c in
   let c = drop_extra_implicit_args sigma c in
   let vars = ref (collect_vars sigma c) in
   let subst = ref [] in
   let rec find_next_evar c = match EConstr.kind sigma c with
     | Evar (evk,args as ev) ->
       (* We skip the test whether args is the identity or not *)
-      let t = existential_type sigma ev in
+      let t = Evarutil.nf_evar sigma (existential_type sigma ev) in
       let t = List.fold_right (fun (e,id) c -> replace_term sigma e id c) !subst t in
       if not (closed0 sigma c) then
 	error "Hints with holes dependent on a bound variable not supported.";
@@ -1435,7 +1430,7 @@ let pr_hints_db (name,db,hintlist) =
 let pr_hint_list_for_head c =
   let dbs = current_db () in
   let validate (name, db) =
-    let hints = List.map (fun v -> 0, v) (Hint_db.map_all Id.Pred.full c db) in
+    let hints = List.map (fun v -> 0, v) (Hint_db.map_all ~secvars:Id.Pred.full c db) in
     (name, db, hints)
   in
   let valid_dbs = List.map validate dbs in
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 467fd46d5..3a0339ff5 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -9,7 +9,6 @@
 open Pp
 open Util
 open Names
-open Term
 open EConstr
 open Environ
 open Globnames
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 309691e39..dce98eed7 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -40,7 +40,6 @@ let mkmeta n = Nameops.make_ident "X" (Some n)
 let meta1 = mkmeta 1
 let meta2 = mkmeta 2
 let meta3 = mkmeta 3
-let meta4 = mkmeta 4
 
 let op2bool = function Some _ -> true | None -> false
 
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index dd09c3a4d..82a3d47b5 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open Evd
 open EConstr
 open Coqlib
diff --git a/tactics/inv.ml b/tactics/inv.ml
index a50ac31e1..5c4b73a62 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -13,7 +13,6 @@ open Names
 open Nameops
 open Term
 open Termops
-open Environ
 open EConstr
 open Vars
 open Namegen
diff --git a/tactics/inv.mli b/tactics/inv.mli
index 446a62f6d..5835e763d 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open EConstr
 open Misctypes
 open Tactypes
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index daa962f1d..83f3da30a 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -260,22 +260,23 @@ let add_inversion_lemma_exn na com comsort bool tac =
 (* Applying a given inversion lemma  *)
 (* ================================= *)
 
-let lemInv id c gls =
+let lemInv id c =
+  Proofview.Goal.enter { enter = begin fun gls ->
   try
-    let open Tacmach in
     let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_unsafe_type_of gls c) in
     let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in
-    Proofview.V82.of_tactic (Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false) gls
+    Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false
   with
     | NoSuchBinding ->
 	user_err 
-	  (hov 0 (pr_econstr_env (Refiner.pf_env gls) (Refiner.project gls) c ++ spc () ++ str "does not refer to an inversion lemma."))
+	  (hov 0 (pr_econstr_env (pf_env gls) (project gls) c ++ spc () ++ str "does not refer to an inversion lemma."))
     | UserError (a,b) ->
 	 user_err ~hdr:"LemInv"
 	   (str "Cannot refine current goal with the lemma " ++
-	      pr_leconstr_env (Refiner.pf_env gls) (Refiner.project gls) c)
+	      pr_leconstr_env (pf_env gls) (project gls) c)
+  end }
 
-let lemInv_gen id c = try_intros_until (fun id -> Proofview.V82.tactic (lemInv id c)) id
+let lemInv_gen id c = try_intros_until (fun id -> lemInv id c) id
 
 let lemInvIn id c ids =
   Proofview.Goal.enter { enter = begin fun gl ->
@@ -289,7 +290,7 @@ let lemInvIn id c ids =
       else
         (tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids))
     in
-    ((tclTHEN (tclTHEN (bring_hyps hyps) (Proofview.V82.tactic (lemInv id c)))
+    ((tclTHEN (tclTHEN (bring_hyps hyps) (lemInv id c))
         (intros_replace_ids)))
   end }
 
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 26d4ac994..a343fc81a 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open EConstr
 open Constrexpr
 open Misctypes
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 5c89331b8..fe9cb123c 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -51,10 +51,8 @@ let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE
 let tclFAIL          = Refiner.tclFAIL
 let tclFAIL_lazy     = Refiner.tclFAIL_lazy
 let tclDO            = Refiner.tclDO
-let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS
 let tclPROGRESS      = Refiner.tclPROGRESS
 let tclSHOWHYPS      = Refiner.tclSHOWHYPS
-let tclNOTSAMEGOAL   = Refiner.tclNOTSAMEGOAL
 let tclTHENTRY       = Refiner.tclTHENTRY
 let tclIFTHENELSE    = Refiner.tclIFTHENELSE
 let tclIFTHENSELSE   = Refiner.tclIFTHENSELSE
@@ -734,13 +732,11 @@ module New = struct
   let case_nodep_then_using =
     general_elim_then_using gl_make_case_nodep false
 
-  let pf_constr_of_global ref tac =
-    Proofview.Goal.enter { enter = begin fun gl ->
-      let env = Proofview.Goal.env gl in
-      let sigma = Tacmach.New.project gl in
-      let (sigma, c) = Evd.fresh_global env sigma ref in
-      let c = EConstr.of_constr c in
-      Proofview.Unsafe.tclEVARS sigma <*> (tac c)
-    end }
+  let pf_constr_of_global ref =
+    Proofview.tclEVARMAP >>= fun sigma ->
+    Proofview.tclENV >>= fun env ->
+    let (sigma, c) = Evd.fresh_global env sigma ref in
+    let c = EConstr.of_constr c in
+    Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT c
 
 end
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index d60196213..96270f748 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -44,10 +44,8 @@ val tclAT_LEAST_ONCE : tactic -> tactic
 val tclFAIL          : int -> std_ppcmds -> tactic
 val tclFAIL_lazy     : int -> std_ppcmds Lazy.t -> tactic
 val tclDO            : int -> tactic -> tactic
-val tclWEAK_PROGRESS : tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclSHOWHYPS      : tactic -> tactic
-val tclNOTSAMEGOAL   : tactic -> tactic
 val tclTHENTRY       : tactic -> tactic -> tactic
 val tclMAP           : ('a -> tactic) -> 'a list -> tactic
 
@@ -265,5 +263,5 @@ module New : sig
   val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args  -> unit Proofview.tactic
   val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args  -> unit Proofview.tactic
 
-  val pf_constr_of_global : Globnames.global_reference -> (constr -> unit Proofview.tactic) -> unit Proofview.tactic
+  val pf_constr_of_global : Globnames.global_reference -> constr Proofview.tactic
 end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d265269b8..11c281985 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -510,6 +510,9 @@ let rec check_mutind env sigma k cl = match EConstr.kind sigma (strip_outer_cast
   else
     let open Context.Rel.Declaration in
     check_mutind (push_rel (LocalAssum (na, c1)) env) sigma (pred k) b
+| LetIn (na, c1, t, b) ->
+    let open Context.Rel.Declaration in
+    check_mutind (push_rel (LocalDef (na, c1, t)) env) sigma k b
 | _ -> error "Not enough products."
 
 (* Refine as a fixpoint *)
@@ -2390,6 +2393,29 @@ let rec explicit_intro_names = function
      explicit_intro_names l
 | [] -> []
 
+let rec check_name_unicity env ok seen = function
+| (_, IntroForthcoming _) :: l -> check_name_unicity env ok seen l
+| (loc, IntroNaming (IntroIdentifier id)) :: l ->
+   (try
+      ignore (if List.mem_f Id.equal id ok then raise Not_found else lookup_named id env);
+      user_err ?loc (pr_id id ++ str" is already used.")
+   with Not_found ->
+     if List.mem_f Id.equal id seen then
+       user_err ?loc (pr_id id ++ str" is used twice.")
+     else
+       check_name_unicity env ok (id::seen) l)
+| (_, IntroAction (IntroOrAndPattern l)) :: l' ->
+    let ll = match l with IntroAndPattern l -> [l] | IntroOrPattern ll -> ll in
+    List.iter (fun l -> check_name_unicity env ok seen (l@l')) ll
+| (_, IntroAction (IntroInjection l)) :: l' ->
+    check_name_unicity env ok seen (l@l')
+| (_, IntroAction (IntroApplyOn (c,pat))) :: l' ->
+    check_name_unicity env ok seen (pat::l')
+| (_, (IntroNaming (IntroAnonymous | IntroFresh _)
+     | IntroAction (IntroWildcard | IntroRewrite _))) :: l ->
+     check_name_unicity env ok seen l
+| [] -> ()
+
 let wild_id = Id.of_string "_tmp"
 
 let rec list_mem_assoc_right id = function
@@ -2525,13 +2551,21 @@ and prepare_intros ?loc with_evars dft destopt = function
   | IntroForthcoming _ -> user_err ?loc 
       (str "Introduction pattern for one hypothesis expected.")
 
+let intro_patterns_head_core with_evars b destopt bound pat =
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    check_name_unicity env [] [] pat;
+    intro_patterns_core with_evars b [] [] [] destopt
+      bound 0 (fun _ l -> clear_wildcards l) pat
+  end }
+
 let intro_patterns_bound_to with_evars n destopt =
-  intro_patterns_core with_evars true [] [] [] destopt
-    (Some (true,n)) 0 (fun _ l -> clear_wildcards l)
+  intro_patterns_head_core with_evars true destopt
+    (Some (true,n))
 
 let intro_patterns_to with_evars destopt =
-  intro_patterns_core with_evars (use_bracketing_last_or_and_intro_pattern ())
-    [] [] [] destopt None 0 (fun _ l -> clear_wildcards l)
+  intro_patterns_head_core with_evars (use_bracketing_last_or_and_intro_pattern ())
+    destopt None
 
 let intro_pattern_to with_evars destopt pat =
   intro_patterns_to with_evars destopt [Loc.tag pat]
@@ -2809,20 +2843,18 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl =
   mkProd_or_LetIn decl cl', sigma'
 
 let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
-  let env = Tacmach.pf_env gl in
-  let ids = Tacmach.pf_ids_of_hyps gl in
-  let sigma, t = Typing.type_of env sigma c in
-  generalize_goal_gen env sigma ids i o t cl
-
-let new_generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
-  let env = Tacmach.New.pf_env gl in
-  let ids = Tacmach.New.pf_ids_of_hyps gl in
+  let open Tacmach.New in
+  let env = pf_env gl in
+  let ids = pf_ids_of_hyps gl in
   let sigma, t = Typing.type_of env sigma c in
   generalize_goal_gen env sigma ids i o t cl
 
-let old_generalize_dep ?(with_let=false) c gl =
+let generalize_dep ?(with_let=false) c =
+  let open Tacmach.New in
+  let open Tacticals.New in
+  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
   let env = pf_env gl in
-  let sign = pf_hyps gl in
+  let sign = Proofview.Goal.hyps gl in
   let sigma = project gl in
   let init_ids = ids_of_named_context (Global.named_context()) in
   let seek (d:named_declaration) (toquant:named_context) =
@@ -2841,11 +2873,11 @@ let old_generalize_dep ?(with_let=false) c gl =
 	  -> id::tothin
       | _ -> tothin
   in
-  let cl' = it_mkNamedProd_or_LetIn (Tacmach.pf_concl gl) to_quantify in
+  let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in
   let body =
     if with_let then
       match EConstr.kind sigma c with
-      | Var id -> id |> Tacmach.pf_get_hyp gl |> NamedDecl.get_value
+      | Var id -> id |> (fun id -> pf_get_hyp id gl) |> NamedDecl.get_value
       | _ -> None
     else None
   in
@@ -2854,20 +2886,19 @@ let old_generalize_dep ?(with_let=false) c gl =
   (** Check that the generalization is indeed well-typed *)
   let (evd, _) = Typing.type_of env evd cl'' in
   let args = Context.Named.to_instance mkVar to_quantify_rev in
-  tclTHENLIST
-    [tclEVARS evd;
-     Proofview.V82.of_tactic (apply_type cl'' (if Option.is_empty body then c::args else args));
-     Proofview.V82.of_tactic (clear (List.rev tothin'))]
-    gl
-
-let generalize_dep ?(with_let = false) c =
-  Proofview.V82.tactic (old_generalize_dep ~with_let c)
+  let tac =
+    tclTHEN
+      (apply_type cl'' (if Option.is_empty body then c::args else args))
+      (clear (List.rev tothin'))
+  in
+  Sigma.Unsafe.of_pair (tac, evd)
+  end }
 
 (**  *)
 let generalize_gen_let lconstr = Proofview.Goal.s_enter { s_enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let newcl, evd =
-    List.fold_right_i (new_generalize_goal gl) 0 lconstr
+    List.fold_right_i (generalize_goal gl) 0 lconstr
       (Tacmach.New.pf_concl gl,Tacmach.New.project gl)
   in
   let (evd, _) = Typing.type_of env evd newcl in
@@ -4189,6 +4220,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_
       let f (_,is_not_let,_,_) = is_not_let in
       Array.map (fun (_,l) -> List.map f l) indsign in
     let names = compute_induction_names branchletsigns names in
+    Array.iter (check_name_unicity env toclear []) names;
     let tac =
     (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn)
       (Tacticals.New.tclTHENLIST [
@@ -4722,7 +4754,7 @@ let symmetry_red allowred =
   | Some eq_data,_,_ ->
       Tacticals.New.tclTHEN
         (convert_concl_no_check concl DEFAULTcast)
-        (Tacticals.New.pf_constr_of_global eq_data.sym apply)
+        (Tacticals.New.pf_constr_of_global eq_data.sym >>= apply)
   | None,eq,eq_kind -> prove_symmetry eq eq_kind
   end }
 
@@ -4818,8 +4850,8 @@ let transitivity_red allowred t =
       Tacticals.New.tclTHEN
         (convert_concl_no_check concl DEFAULTcast)
         (match t with
-	  | None -> Tacticals.New.pf_constr_of_global eq_data.trans eapply
-	  | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans (fun trans -> apply_list [trans;t]))
+	  | None -> Tacticals.New.pf_constr_of_global eq_data.trans >>= eapply
+	  | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans >>= fun trans -> apply_list [trans; t])
    | None,eq,eq_kind ->
       match t with
       | None -> Tacticals.New.tclZEROMSG (str"etransitivity not supported for this relation.")
@@ -4905,7 +4937,7 @@ let shrink_entry sign const =
   } in
   (const, args)
 
-let abstract_subproof id gk tac =
+let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
   let open Tacticals.New in
   let open Tacmach.New in
   let open Proofview.Notations in
@@ -4925,7 +4957,10 @@ let abstract_subproof id gk tac =
 	else (Context.Named.add d s1,s2))
       global_sign (Context.Named.empty, empty_named_context_val) in
   let id = next_global_ident_away id (pf_ids_of_hyps gl) in
-  let concl = it_mkNamedProd_or_LetIn (Proofview.Goal.concl gl) sign in
+  let concl = match goal_type with
+              | None ->  Proofview.Goal.concl gl
+              | Some ty -> ty in
+  let concl = it_mkNamedProd_or_LetIn concl sign in
   let concl =
     try flush_and_check_evars !evdref concl
     with Uninstantiated_evar _ ->
@@ -4955,8 +4990,8 @@ let abstract_subproof id gk tac =
     else (const, List.rev (Context.Named.to_instance Constr.mkVar sign))
   in
   let args = List.map EConstr.of_constr args in
-  let cd = Entries.DefinitionEntry const in
-  let decl = (cd, IsProof Lemma) in
+  let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in
+  let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in
   let cst () =
     (** do not compute the implicit arguments, it may be costly *)
     let () = Impargs.make_implicit_args false in
@@ -4974,18 +5009,21 @@ let abstract_subproof id gk tac =
     Entries.(snd (Future.force const.const_entry_body)) in
   let solve =
     Proofview.tclEFFECTS effs <*>
-    exact_no_check (applist (lem, args))
+    tacK lem args
   in
   let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in
   Sigma.Unsafe.of_pair (tac, evd)
   end }
 
+let abstract_subproof ~opaque id gk tac =
+  cache_term_by_tactic_then ~opaque id gk tac (fun lem args -> exact_no_check (applist (lem, args)))
+
 let anon_id = Id.of_string "anonymous"
 
-let tclABSTRACT name_op tac =
+let name_op_to_name name_op object_kind suffix =
   let open Proof_global in
-  let default_gk = (Global, false, Proof Theorem) in
-  let s, gk = match name_op with
+  let default_gk = (Global, false, object_kind) in
+  match name_op with
     | Some s ->
       (try let _, gk, _ = current_proof_statement () in s, gk
        with NoCurrentProof -> s, default_gk)
@@ -4993,9 +5031,13 @@ let tclABSTRACT name_op tac =
       let name, gk =
 	try let name, gk, _ = current_proof_statement () in name, gk
 	with NoCurrentProof -> anon_id, default_gk in
-      add_suffix name "_subproof", gk
-  in
-  abstract_subproof s gk tac
+      add_suffix name suffix, gk
+
+let tclABSTRACT ?(opaque=true) name_op tac =
+  let s, gk = if opaque
+    then name_op_to_name name_op (Proof Theorem) "_subproof"
+    else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in
+  abstract_subproof ~opaque s gk tac
 
 let unify ?(state=full_transparent_state) x y =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
@@ -5038,10 +5080,6 @@ end
 
 (** Tacticals defined directly in term of Proofview *)
 module New = struct
-  open Proofview.Notations
-
-  let exact_proof c = exact_proof c
-
   open Genredexpr
   open Locus
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index ba4a9706d..07a803542 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -401,7 +401,9 @@ val generalize_dep  : ?with_let:bool (** Don't lose let bindings *) -> constr  -
 
 val unify           : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic
 
-val tclABSTRACT : Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
+val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(constr option) -> Id.t -> Decl_kinds.goal_kind -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic
+
+val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
 
 val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic
 val specialize_eqs : Id.t -> unit Proofview.tactic
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 2c863c42a..726fd23b6 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -49,7 +49,7 @@ struct
     | DNil
 
   (* debug *)
-  let pr_dconstr f : 'a t -> std_ppcmds = function
+  let _pr_dconstr f : 'a t -> std_ppcmds = function
     | DRel -> str "*"
     | DSort -> str "Sort"
     | DRef _ -> str "Ref"