diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-06-14 18:18:37 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-06-15 14:27:06 +0200 |
| commit | db601b06b0880f573b6d1fa83de471679ce87ee7 (patch) | |
| tree | 3efa6f155217f0c7a8a253444eb8e8681bee3de9 /test-suite | |
| parent | 48219205d121ea3093287ac1b887fc81067fac6a (diff) | |
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)
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/3612.v | 1 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3649.v | 2 |
2 files changed, 0 insertions, 3 deletions
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 := |