diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 15 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4763.v | 13 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5097.v | 7 | ||||
| -rw-r--r-- | test-suite/output/ltac.out | 1 | ||||
| -rw-r--r-- | test-suite/output/ltac.v | 5 | ||||
| -rw-r--r-- | test-suite/success/Notations.v | 6 |
6 files changed, 28 insertions, 19 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index f1cb21ecd5..491b16960e 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -84,6 +84,9 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ # All subsystems SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk +PREREQUISITELOG = prerequisite/admit.v.log \ + prerequisite/make_local.v.log prerequisite/make_notation.v.log + ####################################################################### # Phony targets ####################################################################### @@ -221,7 +224,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v fi; \ } > "$@" -$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v +$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \ @@ -253,7 +256,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v fi; \ } > "$@" -$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v +$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -267,7 +270,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v fi; \ } > "$@" -$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out +$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -289,7 +292,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out rm $$tmpoutput; \ } > "$@" -$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v +$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -307,7 +310,7 @@ $(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v # the .v file with exactly two digits after the dot. The reference for # time is a 6120 bogomips cpu. ifneq (,$(bogomips)) -$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v +$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -338,7 +341,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v endif # Ideal-features tests -$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v +$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ diff --git a/test-suite/bugs/closed/4763.v b/test-suite/bugs/closed/4763.v deleted file mode 100644 index ae8ed0e6e8..0000000000 --- a/test-suite/bugs/closed/4763.v +++ /dev/null @@ -1,13 +0,0 @@ -Require Import Coq.Arith.Arith Coq.Classes.Morphisms Coq.Classes.RelationClasses. -Coercion is_true : bool >-> Sortclass. -Global Instance: Transitive leb. -Admitted. - -Goal forall x y z, leb x y -> leb y z -> True. - intros ??? H H'. - lazymatch goal with - | [ H : is_true (?R ?x ?y), H' : is_true (?R ?y ?z) |- _ ] - => pose proof (transitivity H H' : is_true (R x z)) - end. - exact I. -Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/5097.v b/test-suite/bugs/closed/5097.v new file mode 100644 index 0000000000..37b239cf61 --- /dev/null +++ b/test-suite/bugs/closed/5097.v @@ -0,0 +1,7 @@ +(* Tracing existing evars along the weakening rule ("clear") *) +Goal forall y, exists x, x=0->x=y. +intros. +eexists ?[x]. +intros. +let x:=constr:(ltac:(clear y; exact 0)) in idtac x. +Abort. diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index d003c70df9..266e4c7243 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -1,2 +1,3 @@ The command has indeed failed with message: Error: Ltac variable y depends on pattern variable name z which is not bound in current context. +Hx diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v index 7e2610c7d7..e5bcff8ddb 100644 --- a/test-suite/output/ltac.v +++ b/test-suite/output/ltac.v @@ -15,3 +15,8 @@ lazymatch goal with | H1 : HT |- _ => idtac end. Abort. + +(* Check printing of the "var" argument "Hx" *) +Ltac m H := idtac H; exact H. +Goal True. +let a:=constr:(let Hx := 0 in ltac:(m Hx)) in idtac. diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 2f7c62972a..511b60b4bb 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -110,3 +110,9 @@ Goal True -> True. intros H. exact H. Qed. (* Check absence of collision on ".." in nested notations with ".." *) Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)). + +(* Check parsing of { and } is not affected by notations #3479 *) +Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10). +Goal True. +{{ exact I. }} +Qed. |