aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.common2
-rw-r--r--plugins/ltac/coretactics.ml48
-rw-r--r--plugins/ltac/extratactics.ml42
-rw-r--r--plugins/ltac/g_auto.ml42
-rw-r--r--plugins/ltac/g_class.ml42
-rw-r--r--plugins/ltac/g_eqdecide.ml42
-rw-r--r--plugins/ltac/g_rewrite.ml42
-rw-r--r--plugins/ltac/ltac_plugin.mlpack1
-rw-r--r--plugins/ltac/tauto.ml3
-rw-r--r--plugins/ltac/tauto_plugin.mlpack1
-rw-r--r--test-suite/bugs/closed/3612.v1
-rw-r--r--test-suite/bugs/closed/3649.v2
-rw-r--r--theories/Init/Notations.v6
-rw-r--r--theories/Init/Tauto.v2
14 files changed, 14 insertions, 22 deletions
diff --git a/Makefile.common b/Makefile.common
index ec5e6ac85..100698321 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -134,7 +134,7 @@ OTHERSYNTAXCMO:=$(addprefix plugins/syntax/, \
ascii_syntax_plugin.cmo \
string_syntax_plugin.cmo )
DERIVECMO:=plugins/derive/derive_plugin.cmo
-LTACCMO:=plugins/ltac/ltac_plugin.cmo
+LTACCMO:=plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo
SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
SSRCMO:=plugins/ssr/ssreflect_plugin.cmo
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 07b8746fb..50013f558 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 7259faecd..36df25cc7 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 dfd8e88a9..6145e373b 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 905cfd02a..63451210c 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 570cd4e69..dceefeaa1 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 e6ddc5cc1..3e6f42006 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 af1c7149d..12b4c81fc 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 5eacb1a95..bb56fd78a 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 000000000..b3618018e
--- /dev/null
+++ b/plugins/ltac/tauto_plugin.mlpack
@@ -0,0 +1 @@
+Tauto
diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v
index 73709268a..33e5d532a 100644
--- a/test-suite/bugs/closed/3612.v
+++ b/test-suite/bugs/closed/3612.v
@@ -39,7 +39,6 @@ Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P)
p = q.
Declare ML Module "ltac_plugin".
-Declare ML Module "coretactics".
Set Default Proof Mode "Classic".
diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v
index 179f81e66..a664a1ef1 100644
--- a/test-suite/bugs/closed/3649.v
+++ b/test-suite/bugs/closed/3649.v
@@ -3,7 +3,6 @@
(* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0
coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *)
Declare ML Module "ltac_plugin".
-Declare ML Module "coretactics".
Set Default Proof Mode "Classic".
Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
Reserved Notation "x = y" (at level 70, no associativity).
@@ -14,7 +13,6 @@ Axiom admit : forall {T}, T.
Notation "A -> B" := (forall (_ : A), B) : type_scope.
Reserved Infix "o" (at level 40, left associativity).
Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
-Ltac constr_eq a b := let test := constr:(@idpath _ _ : a = b) in idtac.
Global Set Primitive Projections.
Delimit Scope morphism_scope with morphism.
Record PreCategory :=
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index edcd53005..2b0fe1362 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -89,11 +89,5 @@ Open Scope type_scope.
(** ML Tactic Notations *)
Declare ML Module "ltac_plugin".
-Declare ML Module "coretactics".
-Declare ML Module "extratactics".
-Declare ML Module "g_auto".
-Declare ML Module "g_class".
-Declare ML Module "g_eqdecide".
-Declare ML Module "g_rewrite".
Global Set Default Proof Mode "Classic".
diff --git a/theories/Init/Tauto.v b/theories/Init/Tauto.v
index 1e409607a..886533586 100644
--- a/theories/Init/Tauto.v
+++ b/theories/Init/Tauto.v
@@ -2,7 +2,7 @@ Require Import Notations.
Require Import Datatypes.
Require Import Logic.
-Local Declare ML Module "tauto".
+Declare ML Module "tauto_plugin".
Local Ltac not_dep_intros :=
repeat match goal with
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-26 05:06:18 +0000