diff options
| author | Matthieu Sozeau | 2016-03-09 17:11:46 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-03-09 17:11:46 +0100 |
| commit | 2788c86e6a3c089aa7450a7768f8444470e35901 (patch) | |
| tree | 0d0b8c13acd54434536c8030f147e1aff2232dbe /test-suite | |
| parent | b1e6542af576dc92221c4b4eb3e4c547b5901950 (diff) | |
Fix test-suite file coq-prog-args
They were not parsed correctly with a newline in the middle.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/4533.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v index 217ea8a4c7..ae17fb145d 100644 --- a/test-suite/bugs/closed/4533.v +++ b/test-suite/bugs/closed/4533.v @@ -1,5 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." -"Top" "-top" "bug_lex_wrong_rewrite_02") -*- *) +(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_lex_wrong_rewrite_02") -*- *) (* File reduced by coq-bug-finder from original input, then from 1125 lines to 346 lines, then from 360 lines to 346 lines, then from 822 lines to 271 lines, then from 285 lines to 271 lines *) @@ -12,6 +11,7 @@ Tactic Notation "admit" := case proof_admitted. Require Coq.Init.Datatypes. Import Coq.Init.Notations. Global Set Universe Polymorphism. +Global Set Primitive Projections. Notation "A -> B" := (forall (_ : A), B) : type_scope. Module Export Datatypes. Set Implicit Arguments. @@ -202,6 +202,7 @@ Module Type Preserves_Fibers (Os : ReflectiveSubuniverses). Module Export Os_Theory := ReflectiveSubuniverses_Theory Os. End Preserves_Fibers. +Opaque eissect. Module Lex_Reflective_Subuniverses (Os : ReflectiveSubuniverses) (Opf : Preserves_Fibers Os). Import Opf. @@ -221,4 +222,5 @@ v = _) r, match goal with | [ |- p2 @ p0 @ p1 @ eissect (to O A) (g x) = r ] => idtac "good" | [ |- ?G ] => fail 1 "bad" G - end.
\ No newline at end of file + end. + Fail rewrite concat_p_pp.
\ No newline at end of file |