diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 6 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4723.v | 28 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5011.v | 2 | ||||
| -rw-r--r-- | test-suite/output/Arguments.v | 2 | ||||
| -rw-r--r-- | test-suite/success/simpl_tuning.v | 2 |
5 files changed, 35 insertions, 5 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 1dfbb29ff0..a40ea80ae4 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -304,16 +304,16 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ | grep -v "^<W>" \ - | sed -e 's/\s*[0-9]*\.[0-9]\+\s*//g' \ + | sed -e 's/\s*[0-9]*\.[0-9][0-9]*\s*//g' \ -e 's/\s*0\.\s*//g' \ -e 's/\s*[-+]nan\s*//g' \ -e 's/\s*[-+]inf\s*//g' \ > $$tmpoutput; \ - sed -e 's/\s*[0-9]*\.[0-9]\+\s*//g' \ + sed -e 's/\s*[0-9]*\.[0-9][0-9]*\s*//g' \ -e 's/\s*0\.\s*//g' \ -e 's/\s*[-+]nan\s*//g' \ -e 's/\s*[-+]inf\s*//g' \ - $*.out > $$tmpexpected; \ + $*.out > $$tmpexpected; \ diff -b -u $$tmpexpected $$tmpoutput 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ diff --git a/test-suite/bugs/closed/4723.v b/test-suite/bugs/closed/4723.v new file mode 100644 index 0000000000..8884812102 --- /dev/null +++ b/test-suite/bugs/closed/4723.v @@ -0,0 +1,28 @@ + +Require Coq.Program.Tactics. + +Record Matrix (m n : nat). + +Definition kp {m n p q: nat} (A: Matrix m n) (B: Matrix p q): + Matrix (m*p) (n*q). Admitted. + +Fail Program Fact kp_assoc + (xr xc yr yc zr zc: nat) + (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc): + kp x (kp y z) = kp (kp x y) z. + +Ltac Obligation Tactic := admit. +Fail Program Fact kp_assoc + (xr xc yr yc zr zc: nat) + (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc): + kp x (kp y z) = kp (kp x y) z. + +Axiom cheat : forall {A}, A. +Obligation Tactic := apply cheat. + +Program Fact kp_assoc + (xr xc yr yc zr zc: nat) + (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc): + kp x (kp y z) = kp (kp x y) z. +admit. +Admitted.
\ No newline at end of file diff --git a/test-suite/bugs/closed/5011.v b/test-suite/bugs/closed/5011.v new file mode 100644 index 0000000000..c3043ca5d1 --- /dev/null +++ b/test-suite/bugs/closed/5011.v @@ -0,0 +1,2 @@ +Record decoder (n : nat) W := { decode : W -> nat }. +Existing Class decoder. diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v index 05eeaac631..bd9240476f 100644 --- a/test-suite/output/Arguments.v +++ b/test-suite/output/Arguments.v @@ -17,7 +17,7 @@ Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x). Arguments fcomp {_ _ _}%type_scope f g x /. About fcomp. Definition volatile := fun x : nat => x. -Arguments volatile /. +Arguments volatile / _. About volatile. Set Implicit Arguments. Section S1. diff --git a/test-suite/success/simpl_tuning.v b/test-suite/success/simpl_tuning.v index d4191b939b..2728672f30 100644 --- a/test-suite/success/simpl_tuning.v +++ b/test-suite/success/simpl_tuning.v @@ -106,7 +106,7 @@ match goal with |- (f (g x1), h x2) = (f (g x1), h x2) => idtac end. Abort. Definition volatile := fun x : nat => x. -Arguments volatile /. +Arguments volatile / _. Lemma foo : volatile = volatile. simpl. |