diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 10 | ||||
| -rw-r--r-- | test-suite/success/btauto.v | 9 |
2 files changed, 18 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 168a662fd7..928a77cb8e 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -250,11 +250,19 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v # Unit tests ####################################################################### +# An alternative is ifeq ($(OS),Windows_NT) using make's own variable. +ifeq ($(ARCH),win32) + export FINDLIB_SEP=";" +else + export FINDLIB_SEP=":" +endif + # COQLIBINSTALL is quoted in config/make thus we must unquote it, # otherwise the directory name will include the quotes, see # see for example https://stackoverflow.com/questions/10424645/how-to-convert-a-quoted-string-to-a-normal-one-in-makefile + ifeq ($(LOCAL),true) - export OCAMLPATH := $(shell echo $(COQLIBINSTALL):$$OCAMLPATH) + export OCAMLPATH := $(shell echo $(COQLIBINSTALL)$(FINDLIB_SEP)$$OCAMLPATH) endif OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) diff --git a/test-suite/success/btauto.v b/test-suite/success/btauto.v new file mode 100644 index 0000000000..d2512b5cbb --- /dev/null +++ b/test-suite/success/btauto.v @@ -0,0 +1,9 @@ +Require Import Btauto. + +Open Scope bool_scope. + +Lemma test_orb a b : (if a || b then negb (negb b && negb a) else negb a && negb b) = true. +Proof. btauto. Qed. + +Lemma test_xorb a : xorb a a = false. +Proof. btauto. Qed. |