6 files changed, 16 insertions, 15 deletions
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index a299e11f8a..7ecfa57f6d 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -28,7 +28,7 @@ let instantiate_evar evk (ist,rawc) sigma =
   let filtered = Evd.evar_filtered_env evi in
   let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in
   let lvar = {
-    Pretyping.ltac_constrs = constrvars;
+    Glob_term.ltac_constrs = constrvars;
     ltac_uconstrs = Names.Id.Map.empty;
     ltac_idents = Names.Id.Map.empty;
     ltac_genargs = ist.Geninterp.lfun;
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index a971fc79f6..804f734504 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -139,14 +139,16 @@ let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
     end
   | _ -> ElimOnConstr clbind
 
+let mkNumeral n = Numeral (string_of_int (abs n), 0<=n)
+
 let mkTacCase with_evar = function
   | [(clear,ElimOnConstr cl),(None,None),None],None ->
       TacCase (with_evar,(clear,cl))
   (* Reinterpret numbers as a notation for terms *)
   | [(clear,ElimOnAnonHyp n),(None,None),None],None ->
       TacCase (with_evar,
-        (clear,(CAst.make @@ CPrim (Numeral (Bigint.of_int n)),
-	 NoBindings)))
+        (clear,(CAst.make @@ CPrim (mkNumeral n),
+         NoBindings)))
   (* Reinterpret ident as notations for variables in the context *)
   (* because we don't know if they are quantified or not *)
   | [(clear,ElimOnIdent id),(None,None),None],None ->
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 9b6ac8a9ae..67893bd11e 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -386,7 +386,7 @@ type ltac_call_kind =
   | LtacNameCall of ltac_constant
   | LtacAtomCall of glob_atomic_tactic_expr
   | LtacVarCall of Id.t * glob_tactic_expr
-  | LtacConstrInterp of Glob_term.glob_constr * Pretyping.ltac_var_map
+  | LtacConstrInterp of Glob_term.glob_constr * Glob_term.ltac_var_map
 
 type ltac_trace = ltac_call_kind Loc.located list
 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 9d8094205b..0cd3ee2f9c 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -22,7 +22,6 @@ open Nameops
 open Libnames
 open Globnames
 open Nametab
-open Pfedit
 open Refiner
 open Tacmach.New
 open Tactic_debug
@@ -605,10 +604,10 @@ let interp_gen kind ist pattern_mode flags env sigma c =
   let { closure = constrvars ; term } =
     interp_glob_closure ist env sigma ~kind:kind_for_intern ~pattern_mode c in
   let vars = {
-    Pretyping.ltac_constrs = constrvars.typed;
-    Pretyping.ltac_uconstrs = constrvars.untyped;
-    Pretyping.ltac_idents = constrvars.idents;
-    Pretyping.ltac_genargs = ist.lfun;
+    Glob_term.ltac_constrs = constrvars.typed;
+    Glob_term.ltac_uconstrs = constrvars.untyped;
+    Glob_term.ltac_idents = constrvars.idents;
+    Glob_term.ltac_genargs = ist.lfun;
   } in
   (* Jason Gross: To avoid unnecessary modifications to tacinterp, as
       suggested by Arnaud Spiwack, we run push_trace immediately.  We do
@@ -629,7 +628,7 @@ let interp_gen kind ist pattern_mode flags env sigma c =
 let constr_flags () = {
   use_typeclasses = true;
   solve_unification_constraints = true;
-  use_hook = solve_by_implicit_tactic ();
+  use_hook = Pfedit.solve_by_implicit_tactic ();
   fail_evar = true;
   expand_evars = true }
 
@@ -644,14 +643,14 @@ let interp_type = interp_constr_gen IsType
 let open_constr_use_classes_flags () = {
   use_typeclasses = true;
   solve_unification_constraints = true;
-  use_hook = solve_by_implicit_tactic ();
+  use_hook = Pfedit.solve_by_implicit_tactic ();
   fail_evar = false;
   expand_evars = true }
 
 let open_constr_no_classes_flags () = {
   use_typeclasses = false;
   solve_unification_constraints = true;
-  use_hook = solve_by_implicit_tactic ();
+  use_hook = Pfedit.solve_by_implicit_tactic ();
   fail_evar = false;
   expand_evars = true }
 
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index b909c930db..53dc800231 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -364,7 +364,7 @@ let explain_ltac_call_trace last trace loc =
   | Tacexpr.LtacAtomCall te ->
       quote (Pptactic.pr_glob_tactic (Global.env())
               (Tacexpr.TacAtom (Loc.tag te)))
-  | Tacexpr.LtacConstrInterp (c, { Pretyping.ltac_constrs = vars }) ->
+  | Tacexpr.LtacConstrInterp (c, { Glob_term.ltac_constrs = vars }) ->
       quote (Printer.pr_glob_constr_env (Global.env()) c) ++
         (if not (Id.Map.is_empty vars) then
           strbrk " (with " ++
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 5eacb1a95e..2a8ed72387 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -66,7 +66,7 @@ let negation_unfolding = ref true
 (* Whether inner iff are unfolded *)
 let iff_unfolding = ref false
 
-let unfold_iff () = !iff_unfolding || Flags.version_less_or_equal Flags.V8_2
+let unfold_iff () = !iff_unfolding
 
 open Goptions
 let _ =
@@ -79,7 +79,7 @@ let _ =
 
 let _ =
   declare_bool_option
-    { optdepr  = false;
+    { optdepr  = true; (* remove in 8.8 *)
       optname  = "unfolding of iff in intuition";
       optkey   = ["Intuition";"Iff";"Unfolding"];
       optread  = (fun () -> !iff_unfolding);