From f713e6c195d1de177b43cab7c2902f5160f6af9f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 24 Mar 2017 02:18:53 +0100
Subject: A fix to #5414 (ident bound by ltac names now known for "match").

Also taking into account a name in the return clause and in the
indices.

Note the double meaning ``bound as a term to match'' and ``binding in
the "as" clause'' when the term to match is a variable for all of
"match", "if" and "let".
---
 plugins/ltac/evar_tactics.ml | 2 +-
 plugins/ltac/tacexpr.mli     | 2 +-
 plugins/ltac/tacinterp.ml    | 8 ++++----
 plugins/ltac/tactic_debug.ml | 2 +-
 4 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 958f43bd79..4f6f244f82 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/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 85d3944b18..18c9e839ad 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -605,10 +605,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
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 8126421c7d..d495eb8210 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -366,7 +366,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 " ++
-- 
cgit v1.2.3


From f610068823b33bdc0af752a646df05b98489d7ce Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 11 Jun 2017 06:08:02 +0200
Subject: [proof] Deprecate redundant wrappers.

As we would like to reduce the role of proof_global in future
versions, we start to deprecate old compatibility aliases in `Pfedit`
in favor of the real functions underlying the 8.5 proof engine.

We also deprecate a couple of alias types and explicitly mark the few
remaining uses of `Pfedit`.
---
 plugins/ltac/tacinterp.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 85d3944b18..0688d60d41 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
@@ -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 }
 
-- 
cgit v1.2.3


From 0fad09306982a88ff8d633d36abdc440dd542ab3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 13 Jun 2017 10:33:56 +0200
Subject: Dualize the unsafe flag of refine into typecheck and make it
 mandatory.

---
 plugins/ltac/extratactics.ml4 | 2 +-
 plugins/ltac/rewrite.ml       | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 18d7b818cd..7259faecd0 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -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/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 <*>
-- 
cgit v1.2.3


From 571c319ed536cb2757176d3ae4007a75f5d3b04d Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 22 Nov 2016 17:08:14 +0100
Subject: Remove support for Coq 8.2.

---
 plugins/ltac/tauto.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 5eacb1a95e..c6cc955b0f 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 _ =
-- 
cgit v1.2.3


From 5e93f1e95853c3614df813845b94051a45f1a749 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 22 Nov 2016 17:51:32 +0100
Subject: Deprecate options that were introduced for compatibility with 8.2.

---
 plugins/ltac/tauto.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index c6cc955b0f..2a8ed72387 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -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);
-- 
cgit v1.2.3


From d038839a32978548051573286e22462d68d42ee6 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 26 Apr 2016 17:30:30 +0200
Subject: Constrexpr.Numeral stays uninterpreted (string+sign instead of
 BigInt.t)

 This string contains the base-10 representation of the number (big endian)

 Note that some inner parsing stuff still uses bigints, see egramcoq.ml
---
 plugins/ltac/g_tactic.ml4 | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'plugins/ltac')

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 ->
-- 
cgit v1.2.3


From db601b06b0880f573b6d1fa83de471679ce87ee7 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 14 Jun 2017 18:18:37 +0200
Subject: plugins/ltac : avoid spurious .cmxs files

 In the previous setting, all plugins/ltac/*.cmxs except ltac_plugin.cmxs
 (for instance coretactics.cmxs, g_auto.cmxs, ...) were utterly bogus :
  - wrong -for-pack used for their inner .cmx
  - dependency over modules not provided (for instance Tacenv, that ends
    up being a submodule of the pack ltac_plugin).
 But we were lucky, those files were actually never loaded, thanks to the
 several DECLARE PLUGIN inside coretactics and co, that end up in ltac_plugin,
 and hence tell Coq that these modules are already known, preventing
 any attempt to load them.

 Anyway, this commit cleans up this mess (thanks PMP for the help)
---
 plugins/ltac/coretactics.ml4     | 8 ++++----
 plugins/ltac/extratactics.ml4    | 2 +-
 plugins/ltac/g_auto.ml4          | 2 +-
 plugins/ltac/g_class.ml4         | 2 +-
 plugins/ltac/g_eqdecide.ml4      | 2 +-
 plugins/ltac/g_rewrite.ml4       | 2 +-
 plugins/ltac/ltac_plugin.mlpack  | 1 -
 plugins/ltac/tauto.ml            | 3 ++-
 plugins/ltac/tauto_plugin.mlpack | 1 +
 9 files changed, 12 insertions(+), 11 deletions(-)
 create mode 100644 plugins/ltac/tauto_plugin.mlpack

(limited to 'plugins/ltac')

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/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 7259faecd0..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                      *)
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/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/tauto.ml b/plugins/ltac/tauto.ml
index 5eacb1a95e..bb56fd78ac 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 =
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
-- 
cgit v1.2.3