diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-06 17:34:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-17 11:52:38 +0100 |
| commit | ebc0870ca932acf0ceea5fe513e2ca40e74c2a02 (patch) | |
| tree | 4d7d3257b5858bcd2728f678f5cb1f937b2d282e /test-suite/bugs/closed/4533.v | |
| parent | 653de32139ecee3114779a5ee2961c58793889e5 (diff) | |
Moving the Ltac plugin to a pack-based one.
This is cumbersome, because now code may fail at link time if it's not
referring to the correct module name. Therefore, one has to add corresponding
open statements a the top of every file depending on a Ltac module. This
includes seemingly unrelated files that use EXTEND statements.
Diffstat (limited to 'test-suite/bugs/closed/4533.v')
| -rw-r--r-- | test-suite/bugs/closed/4533.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v index ae17fb145..64c7fd8eb 100644 --- a/test-suite/bugs/closed/4533.v +++ b/test-suite/bugs/closed/4533.v @@ -5,6 +5,7 @@ then from 285 lines to 271 lines *) (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0 coqtop version 8.5 (January 2016) *) +Declare ML Module "ltac_plugin". Inductive False := . Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. @@ -223,4 +224,4 @@ v = _) r, | [ |- p2 @ p0 @ p1 @ eissect (to O A) (g x) = r ] => idtac "good" | [ |- ?G ] => fail 1 "bad" G end. - Fail rewrite concat_p_pp.
\ No newline at end of file + Fail rewrite concat_p_pp. |