diff options
author | xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-20 13:28:06 +0000 |
---|---|---|
committer | xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-20 13:28:06 +0000 |
commit | a2bb6f5358df6be7f1089a1a06feaf42a6c81257 (patch) | |
tree | b9b1526f56b675e7f225656439aa022e973bd906 /test-suite | |
parent | f361ba32a28796514b8d3469c7bee3f43ad61fc1 (diff) |
Fix name clash in "failure/inductive.v".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16800 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/Makefile | 32 | ||||
-rw-r--r-- | test-suite/failure/inductive.v | 8 |
2 files changed, 5 insertions, 35 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 29c211de1..5d1f82236 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -65,7 +65,7 @@ log_intro = "==========> TESTING $(1) <==========" COMPLEXITY := $(if $(bogomips),complexity) BUGS := bugs/opened/shouldnotfail bugs/opened/shouldnotsucceed \ - bugs/closed bugs/closed/shouldsucceed bugs/closed/shouldfail + bugs/closed VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ interactive micromega $(COMPLEXITY) modules @@ -197,36 +197,6 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v fi; \ } > "$@" -# Closed bugs that should succeed -$(addsuffix .log,$(wildcard bugs/closed/shouldsucceed/*.v)): %.v.log: %.v - @echo "TEST $<" - $(HIDE){ \ - echo $(call log_intro,$<); \ - $(command) "$<" 2>&1; R=$$?; times; \ - if [ $$R = 0 ]; then \ - echo $(log_success); \ - echo " $<...Ok"; \ - else \ - echo $(log_failure); \ - echo " $<...Error! (bug seems to be opened, please check)"; \ - fi; \ - } > "$@" - -# Closed bugs that should fail -$(addsuffix .log,$(wildcard bugs/closed/shouldfail/*.v)): %.v.log: %.v - @echo "TEST $<" - $(HIDE){ \ - echo $(call log_intro,$<); \ - $(command) "$<" 2>&1; R=$$?; times; \ - if [ $$R = 0 ]; then \ - echo $(log_success); \ - echo " $<...Ok"; \ - else \ - echo $(log_failure); \ - echo " $<...Error! (bug seems to be opened, please check)"; \ - fi; \ - } > "$@" - ####################################################################### # Other generic tests ####################################################################### diff --git a/test-suite/failure/inductive.v b/test-suite/failure/inductive.v index 143e8bb36..f3e47bfd2 100644 --- a/test-suite/failure/inductive.v +++ b/test-suite/failure/inductive.v @@ -15,10 +15,10 @@ Fail Inductive u : Type := d : u | e : t u -> u. Require Import Logic. Require Hurkens. Definition Ti := Type. -Inductive prod (X Y:Ti) := pair : X -> Y -> prod X Y. -Fail Definition B : Prop := let F := prod True in F Prop. (* Aie! *) -(*Definition p2b (P:Prop) : B := pair True Prop I P. -Definition b2p (b:B) : Prop := match b with pair _ P => P end. +Inductive prod2 (X Y:Ti) := pair2 : X -> Y -> prod2 X Y. +Fail Definition B : Prop := let F := prod2 True in F Prop. (* Aie! *) +(*Definition p2b (P:Prop) : B := pair2 True Prop I P. +Definition b2p (b:B) : Prop := match b with pair2 _ P => P end. Lemma L1 : forall A : Prop, b2p (p2b A) -> A. Proof (fun A x => x). Lemma L2 : forall A : Prop, A -> b2p (p2b A). |