Merge remote-tracking branch 'upstream/trunk' into trunk

15 files changed, 32 insertions, 30 deletions

diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 07b8746fb2..50013f5583 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -17,7 +17,7 @@ open Stdarg
 open Extraargs
 open Names
 
-DECLARE PLUGIN "coretactics"
+DECLARE PLUGIN "ltac_plugin"
 
 (** Basic tactics *)
 
@@ -324,11 +324,11 @@ let initial_atomic () =
         "fresh", TacArg(Loc.tag @@ TacFreshId [])
       ]
 
-let () = Mltop.declare_cache_obj initial_atomic "coretactics"
+let () = Mltop.declare_cache_obj initial_atomic "ltac_plugin"
 
 (* First-class Ltac access to primitive blocks *)
 
-let initial_name s = { mltac_plugin = "coretactics"; mltac_tactic = s; }
+let initial_name s = { mltac_plugin = "ltac_plugin"; mltac_tactic = s; }
 let initial_entry s = { mltac_name = initial_name s; mltac_index = 0; }
 
 let register_list_tactical name f =
@@ -356,4 +356,4 @@ let initial_tacticals () =
     "solve", TacFun ([Name (idn 0)], TacML (None, (initial_entry "solve", [varn 0])));
   ]
 
-let () = Mltop.declare_cache_obj initial_tacticals "coretactics"
+let () = Mltop.declare_cache_obj initial_tacticals "ltac_plugin"
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/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 18d7b818cd..36df25cc77 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -28,7 +28,7 @@ open Equality
 open Misctypes
 open Proofview.Notations
 
-DECLARE PLUGIN "extratactics"
+DECLARE PLUGIN "ltac_plugin"
 
 (**********************************************************************)
 (* replace, discriminate, injection, simplify_eq                      *)
@@ -365,7 +365,7 @@ let refine_tac ist simple with_classes c =
     let update = begin fun sigma ->
       c env sigma
     end in
-    let refine = Refine.refine ~unsafe:true update in
+    let refine = Refine.refine ~typecheck:false update in
     if simple then refine
     else refine <*>
            Tactics.New.reduce_after_refine <*>
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index dfd8e88a91..6145e373b1 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -18,7 +18,7 @@ open Pcoq.Constr
 open Pltac
 open Hints
 
-DECLARE PLUGIN "g_auto"
+DECLARE PLUGIN "ltac_plugin"
 
 (* Hint bases *)
 
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index 905cfd02a6..63451210ca 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -13,7 +13,7 @@ open Class_tactics
 open Stdarg
 open Tacarg
 
-DECLARE PLUGIN "g_class"
+DECLARE PLUGIN "ltac_plugin"
 
 (** Options: depth, debug and transparency settings. *)
 
diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4
index 570cd4e694..dceefeaa13 100644
--- a/plugins/ltac/g_eqdecide.ml4
+++ b/plugins/ltac/g_eqdecide.ml4
@@ -17,7 +17,7 @@
 open API
 open Eqdecide
 
-DECLARE PLUGIN "g_eqdecide"
+DECLARE PLUGIN "ltac_plugin"
 
 TACTIC EXTEND decide_equality
 | [ "decide" "equality" ] -> [ decideEqualityGoal ]
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index e6ddc5cc1b..3e6f420065 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -27,7 +27,7 @@ open Pcoq.Prim
 open Pcoq.Constr
 open Pltac
 
-DECLARE PLUGIN "g_rewrite"
+DECLARE PLUGIN "ltac_plugin"
 
 type constr_expr_with_bindings = constr_expr with_bindings
 type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings
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/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack
index af1c7149da..12b4c81fc4 100644
--- a/plugins/ltac/ltac_plugin.mlpack
+++ b/plugins/ltac/ltac_plugin.mlpack
@@ -21,7 +21,6 @@ G_auto
 G_class
 Rewrite
 G_rewrite
-Tauto
 G_eqdecide
 G_tactic
 G_ltac
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 3927ca7ce1..fad181c897 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1539,7 +1539,7 @@ let assert_replacing id newt tac =
     | d :: rem -> insert_dependent env sigma (LocalAssum (NamedDecl.get_id d, newt)) [] after @ rem
     in
     let env' = Environ.reset_with_named_context (val_of_named_context nc) env in
-    Refine.refine ~unsafe:false begin fun sigma ->
+    Refine.refine ~typecheck:true begin fun sigma ->
       let (sigma, ev) = Evarutil.new_evar env' sigma concl in
       let (sigma, ev') = Evarutil.new_evar env sigma newt in
       let map d =
@@ -1573,7 +1573,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
 	match clause, prf with
 	| Some id, Some p ->
             let tac = tclTHENLIST [
-              Refine.refine ~unsafe:false (fun h -> (h,p));
+              Refine.refine ~typecheck:true (fun h -> (h,p));
               Proofview.Unsafe.tclNEWGOALS gls;
             ] in
             Proofview.Unsafe.tclEVARS undef <*>
@@ -1590,7 +1590,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
               let (sigma, ev) = Evarutil.new_evar env sigma newt in
               (sigma, mkApp (p, [| ev |]))
             end in
-            Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls
+            Refine.refine ~typecheck:true make <*> Proofview.Unsafe.tclNEWGOALS gls
             end
 	| None, None ->
             Proofview.Unsafe.tclEVARS undef <*>
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..71f7082e70 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -13,13 +13,14 @@ open Hipattern
 open Names
 open Geninterp
 open Misctypes
+open Ltac_plugin
 open Tacexpr
 open Tacinterp
 open Util
 open Tacticals.New
 open Proofview.Notations
 
-let tauto_plugin = "tauto"
+let tauto_plugin = "tauto_plugin"
 let () = Mltop.add_known_module tauto_plugin
 
 let assoc_var s ist =
@@ -66,7 +67,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 +80,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);
diff --git a/plugins/ltac/tauto_plugin.mlpack b/plugins/ltac/tauto_plugin.mlpack
new file mode 100644
index 0000000000..b3618018ea
--- /dev/null
+++ b/plugins/ltac/tauto_plugin.mlpack
@@ -0,0 +1 @@
+Tauto