diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 11 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_10894.v | 12 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_10904.v | 8 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_6323.v | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_9851.v | 18 | ||||
| -rw-r--r-- | test-suite/ltac2/ltac2env.v | 15 | ||||
| -rwxr-xr-x | test-suite/misc/votour.sh | 3 | ||||
| -rw-r--r-- | test-suite/output/locate.out | 3 | ||||
| -rw-r--r-- | test-suite/output/locate.v | 3 |
9 files changed, 71 insertions, 5 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index c0bdb29fab..c60f39231e 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -32,18 +32,21 @@ include ../Makefile.common # Variables ####################################################################### -# Default value when called from a freshly compiled Coq, but can be -# easily overridden - +ifneq ($(wildcard ../_build),) +BIN:=$(shell cd ..; pwd)/_build/install/default/bin/ +COQLIB:=$(shell cd ..; pwd)/_build/install/default/lib/coq +else BIN := $(shell cd ..; pwd)/bin/ -COQFLAGS?= COQLIB?= ifeq ($(COQLIB),) COQLIB := $(shell ocaml ocaml_pwd.ml ..) endif +endif # exists ../_build export COQLIB +COQFLAGS?= + coqc := $(BIN)coqc -q -R prerequisite TestSuite $(COQFLAGS) coqchk := $(BIN)coqchk -R prerequisite TestSuite coqdoc := $(BIN)coqdoc diff --git a/test-suite/bugs/closed/bug_10894.v b/test-suite/bugs/closed/bug_10894.v new file mode 100644 index 0000000000..b8c9367951 --- /dev/null +++ b/test-suite/bugs/closed/bug_10894.v @@ -0,0 +1,12 @@ +(* Check that uconstrs are interpreted in the ltac-substituted environment *) +(* Was a regression introduced in 4dab4fc (#7288) *) + +Tactic Notation "bind" hyp(x) "in" uconstr(f) "as" ident(h) := + set (h := fun x => f). + +Fact test : nat -> nat. +Proof. + intros n. + bind n in (n*n) as f. + assert (f 0 = 0) by reflexivity. +Abort. diff --git a/test-suite/bugs/closed/bug_10904.v b/test-suite/bugs/closed/bug_10904.v new file mode 100644 index 0000000000..32b25ff726 --- /dev/null +++ b/test-suite/bugs/closed/bug_10904.v @@ -0,0 +1,8 @@ +Definition a := fun (P:SProp) (p:P) => p. + +Lemma foo : (let k := a in let k' := a in fun (x:nat) y => x) = (let k := a in fun x y => y). +Proof. + Fail reflexivity. + match goal with |- ?l = _ => exact_no_check (eq_refl l) end. +Fail Qed. +Abort. diff --git a/test-suite/bugs/closed/bug_6323.v b/test-suite/bugs/closed/bug_6323.v index fdc33befc6..24feb7155c 100644 --- a/test-suite/bugs/closed/bug_6323.v +++ b/test-suite/bugs/closed/bug_6323.v @@ -6,4 +6,5 @@ Goal True. simple refine (let id' : { x : X' | True } -> X' := _ in _); [ abstract refine (@proj1_sig _ _) | ] ]. -Abort. + exact I. +Defined. diff --git a/test-suite/bugs/closed/bug_9851.v b/test-suite/bugs/closed/bug_9851.v new file mode 100644 index 0000000000..1f57ce8471 --- /dev/null +++ b/test-suite/bugs/closed/bug_9851.v @@ -0,0 +1,18 @@ +Require Import Ring_base. +Record word : Type := Build_word + { rep : Type; + zero : rep; one: rep; + add : rep -> rep -> rep; + sub : rep -> rep -> rep; + opp : rep -> rep; + mul : rep -> rep -> rep; + }. +Axiom rth + : forall (word : word ), + @ring_theory (@rep word) + (@zero word) + (@one word) (@add word) + (@mul word) (@sub word) + (@opp word) (@eq (@rep word)). + +Fail Add Ring wring: (@rth _). diff --git a/test-suite/ltac2/ltac2env.v b/test-suite/ltac2/ltac2env.v new file mode 100644 index 0000000000..743e62932d --- /dev/null +++ b/test-suite/ltac2/ltac2env.v @@ -0,0 +1,15 @@ +Require Import Ltac2.Ltac2. + +Ltac2 get_opt o := match o with None => Control.throw Not_found | Some x => x end. + +Goal True. +Proof. +(* Fails at runtime because not fully applied *) +Fail ltac1:(ltac2:(x |- ())). +(* Type mismatch: Ltac1.t vs. constr *) +Fail ltac1:(ltac2:(x |- pose $x)). +(* Check that runtime cast is OK *) +ltac1:(let t := ltac2:(x |- let c := (get_opt (Ltac1.to_constr x)) in pose $c) in t nat). +(* Type mismatch *) +Fail ltac1:(let t := ltac2:(x |- let c := (get_opt (Ltac1.to_constr x)) in pose $c) in t ident:(foo)). +Abort. diff --git a/test-suite/misc/votour.sh b/test-suite/misc/votour.sh new file mode 100755 index 0000000000..ac26aed49b --- /dev/null +++ b/test-suite/misc/votour.sh @@ -0,0 +1,3 @@ +command -v "${BIN}votour" || { echo "Missing votour"; exit 1; } + +"${BIN}votour" prerequisite/ssr_mini_mathcomp.vo < /dev/null diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out new file mode 100644 index 0000000000..473db2d312 --- /dev/null +++ b/test-suite/output/locate.out @@ -0,0 +1,3 @@ +Notation +"b1 && b2" := if b1 then b2 else false (default interpretation) +"x && y" := andb x y : bool_scope diff --git a/test-suite/output/locate.v b/test-suite/output/locate.v new file mode 100644 index 0000000000..af8b0ee193 --- /dev/null +++ b/test-suite/output/locate.v @@ -0,0 +1,3 @@ +Set Printing Width 400. +Notation "b1 && b2" := (if b1 then b2 else false). +Locate "&&". |