diff options
Diffstat (limited to 'test-suite')
24 files changed, 366 insertions, 91 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index aca7ab0b28..0d8a6ebed7 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -49,7 +49,8 @@ endif endif # exists ../_build export COQLIB -COQFLAGS?= +COQEXTRAFLAGS?= +COQFLAGS?=$(COQEXTRAFLAGS) coqc := $(BIN)coqc -q -R prerequisite TestSuite $(COQFLAGS) coqchk := $(BIN)coqchk -R prerequisite TestSuite @@ -416,14 +417,16 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) $(HIDE){ \ echo $(call log_intro,$<); \ output=$*.out.real; \ + export LC_CTYPE=C; \ + export LANG=C; \ $(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \ - | grep -v "Welcome to Coq" \ - | grep -v "\[Loading ML file" \ - | grep -v "Skipping rcfile loading" \ - | grep -v "^<W>" \ + | grep -a -v "Welcome to Coq" \ + | grep -a -v "\[Loading ML file" \ + | grep -a -v "Skipping rcfile loading" \ + | grep -a -v "^<W>" \ | sed 's/File "[^"]*"/File "stdin"/' \ > $$output; \ - diff -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \ + diff -a -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ diff --git a/test-suite/bugs/closed/HoTT_coq_010.v b/test-suite/bugs/closed/HoTT_coq_010.v index 42b1244fb5..caa7373f5e 100644 --- a/test-suite/bugs/closed/HoTT_coq_010.v +++ b/test-suite/bugs/closed/HoTT_coq_010.v @@ -1,3 +1,3 @@ -SearchAbout and. +Search and. (* Anomaly: Mismatched instance and context when building universe substitution. Please report. *) diff --git a/test-suite/bugs/closed/bug_11845.v b/test-suite/bugs/closed/bug_11845.v new file mode 100644 index 0000000000..d27f8c4ef0 --- /dev/null +++ b/test-suite/bugs/closed/bug_11845.v @@ -0,0 +1,6 @@ + +Module Type T. Parameter Inline v : Prop. End T. + +Module F(A:T). End F. + +Fail Include F. diff --git a/test-suite/bugs/closed/bug_11846.v b/test-suite/bugs/closed/bug_11846.v new file mode 100644 index 0000000000..53517e7703 --- /dev/null +++ b/test-suite/bugs/closed/bug_11846.v @@ -0,0 +1,16 @@ +Require Import FunInd. + +Inductive tree : Type := +| Node : unit -> tree. + +Definition height (s : tree) : unit := +match s with +| Node h => h +end. + +Definition bal : forall l, let h := height l in tree := fun l => + let h := height l in + Node h. + +Set Warnings "+all". +Functional Scheme bal_ind := Induction for bal Sort Prop. diff --git a/test-suite/bugs/closed/bug_11890.v b/test-suite/bugs/closed/bug_11890.v new file mode 100644 index 0000000000..c0426fcfda --- /dev/null +++ b/test-suite/bugs/closed/bug_11890.v @@ -0,0 +1,10 @@ +Require Import Coq.Structures.Orders Coq.ZArith.ZArith Coq.Sorting.Mergesort. +(* Note that this has always worked fine without the '; we are testing importing notations from the stdlib here *) +Declare Module A : LeBool'. +Declare Module B : LtBool'. +Import A B NatOrder. +(* +Error: Notation "_ <=? _" is already defined at level 70 with arguments constr +at next level, constr at next level while it is now required to be at level 35 +with arguments constr at next level, constr at next level. +*) diff --git a/test-suite/bugs/closed/bug_3900.v b/test-suite/bugs/closed/bug_3900.v index 6be2161c2f..ddede74acc 100644 --- a/test-suite/bugs/closed/bug_3900.v +++ b/test-suite/bugs/closed/bug_3900.v @@ -9,5 +9,5 @@ Variable Pmor : forall s d : obj, morphism A (projT1 s) (projT1 d) -> Type. Class Foo (x : Type) := { _ : forall y, y }. Local Instance ishset_pmor {s d m} : Foo (Pmor s d m). Proof. -SearchAbout ((forall _ _, _) -> Foo _). +Search ((forall _ _, _) -> Foo _). Abort. diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh index 8f9ab9a711..3ffe831b3c 100755 --- a/test-suite/coq-makefile/native1/run.sh +++ b/test-suite/coq-makefile/native1/run.sh @@ -1,7 +1,7 @@ #!/usr/bin/env bash -NATIVECOMP=$(grep "let no_native_compiler = false" ../../../config/coq_config.ml)||true -if [[ $(which ocamlopt) && $NATIVECOMP ]]; then +NONATIVECOMP=$(grep "let native_compiler = false" ../../../config/coq_config.ml)||true +if [[ $(which ocamlopt) && ! $NONATIVECOMP ]]; then . ../template/init.sh diff --git a/test-suite/coq-makefile/native2/_CoqProject b/test-suite/coq-makefile/native2/_CoqProject new file mode 100644 index 0000000000..61136e82f0 --- /dev/null +++ b/test-suite/coq-makefile/native2/_CoqProject @@ -0,0 +1,10 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mlpack +src/test.mlg +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/native2/run.sh b/test-suite/coq-makefile/native2/run.sh new file mode 100755 index 0000000000..857f70fdff --- /dev/null +++ b/test-suite/coq-makefile/native2/run.sh @@ -0,0 +1,33 @@ +#!/usr/bin/env bash + +NONATIVECOMP=$(grep "let native_compiler = false" ../../../config/coq_config.ml)||true +if [[ $(which ocamlopt) && ! $NONATIVECOMP ]]; then + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf +COQEXTRAFLAGS="-native-compiler yes" make +make html mlihtml +make install DSTROOT="$PWD/tmp" +#make debug +(cd "$(find tmp -name user-contrib)" && find .) | sort > actual +sort > desired <<EOT +. +./test +./test/test.glob +./test/test_plugin.cmi +./test/test_plugin.cmx +./test/test_plugin.cmxa +./test/test_plugin.cmxs +./test/test.v +./test/test.vo +./test/.coq-native +./test/.coq-native/Ntest_test.cmi +./test/.coq-native/Ntest_test.cmx +./test/.coq-native/Ntest_test.cmxs +EOT +exec diff -u desired actual + +fi +exit 0 # test skipped diff --git a/test-suite/output/FloatExtraction.out b/test-suite/output/FloatExtraction.out index cfd6633752..dd8189c56f 100644 --- a/test-suite/output/FloatExtraction.out +++ b/test-suite/output/FloatExtraction.out @@ -1,3 +1,17 @@ +File "stdin", line 25, characters 8-12: +Warning: The constant 0.01 is not a binary64 floating-point value. A closest +value will be used and unambiguously printed 0.01. [inexact-float,parsing] +File "stdin", line 25, characters 20-25: +Warning: The constant -0.01 is not a binary64 floating-point value. A closest +value will be used and unambiguously printed -0.01. [inexact-float,parsing] +File "stdin", line 25, characters 27-35: +Warning: The constant 1.7e+308 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed 1.6999999999999999e+308. +[inexact-float,parsing] +File "stdin", line 25, characters 37-46: +Warning: The constant -1.7e-308 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed +-1.7000000000000002e-308. [inexact-float,parsing] (** val infinity : Float64.t **) diff --git a/test-suite/output/FloatSyntax.out b/test-suite/output/FloatSyntax.out index 668a55977d..7941d2e647 100644 --- a/test-suite/output/FloatSyntax.out +++ b/test-suite/output/FloatSyntax.out @@ -4,8 +4,16 @@ : float (-2.5)%float : float +File "stdin", line 9, characters 6-13: +Warning: The constant 2.5e123 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed 2.4999999999999999e+123. +[inexact-float,parsing] 2.4999999999999999e+123%float : float +File "stdin", line 10, characters 7-16: +Warning: The constant -2.5e-123 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed +-2.5000000000000001e-123. [inexact-float,parsing] (-2.5000000000000001e-123)%float : float (2 + 2)%float @@ -18,14 +26,34 @@ : float -2.5 : float +File "stdin", line 19, characters 6-13: +Warning: The constant 2.5e123 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed 2.4999999999999999e+123. +[inexact-float,parsing] 2.4999999999999999e+123 : float +File "stdin", line 20, characters 7-16: +Warning: The constant -2.5e-123 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed +-2.5000000000000001e-123. [inexact-float,parsing] -2.5000000000000001e-123 : float 2 + 2 : float 2.5 + 2.5 : float +File "stdin", line 24, characters 6-11: +Warning: The constant 1e309 is not a binary64 floating-point value. A closest +value will be used and unambiguously printed infinity. +[inexact-float,parsing] +infinity + : float +File "stdin", line 25, characters 6-12: +Warning: The constant -1e309 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed neg_infinity. +[inexact-float,parsing] +neg_infinity + : float 2 : nat 2%float diff --git a/test-suite/output/FloatSyntax.v b/test-suite/output/FloatSyntax.v index 85f611352c..eca712db10 100644 --- a/test-suite/output/FloatSyntax.v +++ b/test-suite/output/FloatSyntax.v @@ -21,6 +21,9 @@ Check (-2.5e-123). Check (2 + 2). Check (2.5 + 2.5). +Check 1e309. +Check -1e309. + Open Scope nat_scope. Check 2. diff --git a/test-suite/output/NoAxiomFromR.v b/test-suite/output/NoAxiomFromR.v index 9cf6879699..7abbe29452 100644 --- a/test-suite/output/NoAxiomFromR.v +++ b/test-suite/output/NoAxiomFromR.v @@ -5,6 +5,6 @@ Inductive TT : Set := Lemma lem4 : forall (n m : nat), S m <= m -> C (S m) <> C n -> False. -Proof. firstorder. Qed. +Proof. firstorder lia. Qed. Print Assumptions lem4. diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out index 113384e9cf..060877707b 100644 --- a/test-suite/output/NumeralNotations.out +++ b/test-suite/output/NumeralNotations.out @@ -218,3 +218,19 @@ let v : ty := Build_ty Set set in v : ty : ty let v : ty := Build_ty Type type in v : ty : ty +1 + : nat +(-1000)%Z + : Z +0 + : Prop ++0 + : bool +-0 + : bool +00 + : nat * nat +1000 + : Prop +1_000 + : list nat diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v index 22aff36d67..47e1b127cb 100644 --- a/test-suite/output/NumeralNotations.v +++ b/test-suite/output/NumeralNotations.v @@ -457,3 +457,33 @@ Module Test20. Check let v := 4%kt in v : ty. Check let v := 5%kt in v : ty. End Test20. + +Module Test21. + + Check 00001. + Check (-1_000)%Z. + +End Test21. + +Module Test22. + +Notation "0" := False. +Notation "+0" := true. +Notation "-0" := false. +Notation "00" := (0%nat, 0%nat). +Check 0. +Check +0. +Check -0. +Check 00. + +Notation "1000" := True. +Notation "1_000" := (cons 1 nil). +Check 1000. +Check 1_000. + +(* To do: preserve parsing of -0: +Require Import ZArith. +Check (-0)%Z. +*) + +End Test22. diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index 4f09f00c56..bdfa8afb6a 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -4,7 +4,7 @@ fun '(x, y) => (y, x) : A * B -> B * A forall '(x, y), swap (x, y) = (y, x) : Prop -proj_informative = fun '(exist _ x _) => x : A +proj_informative = fun '(exist _ x _) => x : {x : A | P x} -> A foo = fun '(Bar n b tt p) => if b then n + p else n - p : Foo -> nat @@ -29,8 +29,7 @@ exists '(x, y) '(z, w), swap (x, y) = (z, w) ∀ '(x, y), swap (x, y) = (y, x) : Prop both_z = -fun pat : nat * nat => -let '(n, p) as x := pat return (F x) in (Z n, Z p) : F (n, p) +fun pat : nat * nat => let '(n, p) as x := pat return (F x) in (Z n, Z p) : forall pat : nat * nat, F pat fun '(x, y) '(z, t) => swap (x, y) = (z, t) : A * B -> B * A -> Prop diff --git a/test-suite/output/QArithSyntax.out b/test-suite/output/QArithSyntax.out index 6bc04f1cef..fe6a1d25c6 100644 --- a/test-suite/output/QArithSyntax.out +++ b/test-suite/output/QArithSyntax.out @@ -1,14 +1,14 @@ -eq_refl : 102e-2 = 102e-2 - : 102e-2 = 102e-2 -eq_refl : 102e-1 = 102e-1 - : 102e-1 = 102e-1 +eq_refl : 1.02 = 1.02 + : 1.02 = 1.02 +eq_refl : 10.2 = 10.2 + : 10.2 = 10.2 eq_refl : 1020 = 1020 : 1020 = 1020 eq_refl : 102 = 102 : 102 = 102 -eq_refl : 102e-2 = 102e-2 - : 102e-2 = 102e-2 +eq_refl : 1.02 = 1.02 + : 1.02 = 1.02 eq_refl : -1e-4 = -1e-4 : -1e-4 = -1e-4 -eq_refl : -50e-2 = -50e-2 - : -50e-2 = -50e-2 +eq_refl : -0.50 = -0.50 + : -0.50 = -0.50 diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out index 2b14ca7069..1685964b0f 100644 --- a/test-suite/output/RealSyntax.out +++ b/test-suite/output/RealSyntax.out @@ -2,19 +2,21 @@ : R (-31)%R : R -15e-1%R +1.5%R : R -eq_refl : 102e-2 = 102e-2 - : 102e-2 = 102e-2 -eq_refl : 102e-1 = 102e-1 - : 102e-1 = 102e-1 +15%R + : R +eq_refl : 1.02 = 1.02 + : 1.02 = 1.02 +eq_refl : 10.2 = 10.2 + : 10.2 = 10.2 eq_refl : 102e1 = 102e1 : 102e1 = 102e1 eq_refl : 102 = 102 : 102 = 102 -eq_refl : 102e-2 = 102e-2 - : 102e-2 = 102e-2 +eq_refl : 1.02 = 1.02 + : 1.02 = 1.02 eq_refl : -1e-4 = -1e-4 : -1e-4 = -1e-4 -eq_refl : -50e-2 = -50e-2 - : -50e-2 = -50e-2 +eq_refl : -0.50 = -0.50 + : -0.50 = -0.50 diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v index 7be8b18ac8..e5f9d06316 100644 --- a/test-suite/output/RealSyntax.v +++ b/test-suite/output/RealSyntax.v @@ -3,6 +3,7 @@ Check 32%R. Check (-31)%R. Check 1.5_%R. +Check 1_.5_e1_%R. Open Scope R_scope. diff --git a/test-suite/output/allBytes.out b/test-suite/output/allBytes.out new file mode 100644 index 0000000000..8d188c4c45 --- /dev/null +++ b/test-suite/output/allBytes.out @@ -0,0 +1 @@ +!"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ diff --git a/test-suite/output/allBytes.v b/test-suite/output/allBytes.v new file mode 100644 index 0000000000..01a5161ef4 --- /dev/null +++ b/test-suite/output/allBytes.v @@ -0,0 +1,121 @@ +(* Taken from bedrock2 *) + +(* Note: not an utf8 file *) + +Require Import Coq.ZArith.BinInt Coq.Lists.List. +Require Coq.Init.Byte Coq.Strings.Byte Coq.Strings.String. + +Definition allBytes: list Byte.byte := + map (fun nn => match Byte.of_N (BinNat.N.of_nat nn) with + | Some b => b + | None => Byte.x00 (* won't happen *) + end) + (seq 32 95). + +Notation "a b" := (@cons Byte.byte a b) + (only printing, right associativity, at level 3, format "a b"). + +Notation "" := (@nil Byte.byte) + (only printing, right associativity, at level 3, format ""). + +Notation " " := (Byte.x20) (only printing). +Notation "'!'" := (Byte.x21) (only printing). +Notation "'""'" := (Byte.x22) (only printing). +Notation "'#'" := (Byte.x23) (only printing). +Notation "'$'" := (Byte.x24) (only printing). +Notation "'%'" := (Byte.x25) (only printing). +Notation "'&'" := (Byte.x26) (only printing). +Notation "'''" := (Byte.x27) (only printing). +Notation "'('" := (Byte.x28) (only printing). +Notation "')'" := (Byte.x29) (only printing). +Notation "'*'" := (Byte.x2a) (only printing). +Notation "'+'" := (Byte.x2b) (only printing). +Notation "','" := (Byte.x2c) (only printing). +Notation "'-'" := (Byte.x2d) (only printing). +Notation "'.'" := (Byte.x2e) (only printing). +Notation "'/'" := (Byte.x2f) (only printing). +Notation "'0'" := (Byte.x30) (only printing). +Notation "'1'" := (Byte.x31) (only printing). +Notation "'2'" := (Byte.x32) (only printing). +Notation "'3'" := (Byte.x33) (only printing). +Notation "'4'" := (Byte.x34) (only printing). +Notation "'5'" := (Byte.x35) (only printing). +Notation "'6'" := (Byte.x36) (only printing). +Notation "'7'" := (Byte.x37) (only printing). +Notation "'8'" := (Byte.x38) (only printing). +Notation "'9'" := (Byte.x39) (only printing). +Notation "':'" := (Byte.x3a) (only printing). +Notation "';'" := (Byte.x3b) (only printing). +Notation "'<'" := (Byte.x3c) (only printing). +Notation "'='" := (Byte.x3d) (only printing). +Notation "'>'" := (Byte.x3e) (only printing). +Notation "'?'" := (Byte.x3f) (only printing). +Notation "'@'" := (Byte.x40) (only printing). +Notation "'A'" := (Byte.x41) (only printing). +Notation "'B'" := (Byte.x42) (only printing). +Notation "'C'" := (Byte.x43) (only printing). +Notation "'D'" := (Byte.x44) (only printing). +Notation "'E'" := (Byte.x45) (only printing). +Notation "'F'" := (Byte.x46) (only printing). +Notation "'G'" := (Byte.x47) (only printing). +Notation "'H'" := (Byte.x48) (only printing). +Notation "'I'" := (Byte.x49) (only printing). +Notation "'J'" := (Byte.x4a) (only printing). +Notation "'K'" := (Byte.x4b) (only printing). +Notation "'L'" := (Byte.x4c) (only printing). +Notation "'M'" := (Byte.x4d) (only printing). +Notation "'N'" := (Byte.x4e) (only printing). +Notation "'O'" := (Byte.x4f) (only printing). +Notation "'P'" := (Byte.x50) (only printing). +Notation "'Q'" := (Byte.x51) (only printing). +Notation "'R'" := (Byte.x52) (only printing). +Notation "'S'" := (Byte.x53) (only printing). +Notation "'T'" := (Byte.x54) (only printing). +Notation "'U'" := (Byte.x55) (only printing). +Notation "'V'" := (Byte.x56) (only printing). +Notation "'W'" := (Byte.x57) (only printing). +Notation "'X'" := (Byte.x58) (only printing). +Notation "'Y'" := (Byte.x59) (only printing). +Notation "'Z'" := (Byte.x5a) (only printing). +Notation "'['" := (Byte.x5b) (only printing). +Notation "'\'" := (Byte.x5c) (only printing). +Notation "']'" := (Byte.x5d) (only printing). +Notation "'^'" := (Byte.x5e) (only printing). +Notation "'_'" := (Byte.x5f) (only printing). +Notation "'`'" := (Byte.x60) (only printing). +Notation "'a'" := (Byte.x61) (only printing). +Notation "'b'" := (Byte.x62) (only printing). +Notation "'c'" := (Byte.x63) (only printing). +Notation "'d'" := (Byte.x64) (only printing). +Notation "'e'" := (Byte.x65) (only printing). +Notation "'f'" := (Byte.x66) (only printing). +Notation "'g'" := (Byte.x67) (only printing). +Notation "'h'" := (Byte.x68) (only printing). +Notation "'i'" := (Byte.x69) (only printing). +Notation "'j'" := (Byte.x6a) (only printing). +Notation "'k'" := (Byte.x6b) (only printing). +Notation "'l'" := (Byte.x6c) (only printing). +Notation "'m'" := (Byte.x6d) (only printing). +Notation "'n'" := (Byte.x6e) (only printing). +Notation "'o'" := (Byte.x6f) (only printing). +Notation "'p'" := (Byte.x70) (only printing). +Notation "'q'" := (Byte.x71) (only printing). +Notation "'r'" := (Byte.x72) (only printing). +Notation "'s'" := (Byte.x73) (only printing). +Notation "'t'" := (Byte.x74) (only printing). +Notation "'u'" := (Byte.x75) (only printing). +Notation "'v'" := (Byte.x76) (only printing). +Notation "'w'" := (Byte.x77) (only printing). +Notation "'x'" := (Byte.x78) (only printing). +Notation "'y'" := (Byte.x79) (only printing). +Notation "'z'" := (Byte.x7a) (only printing). +Notation "'{'" := (Byte.x7b) (only printing). +Notation "'|'" := (Byte.x7c) (only printing). +Notation "'}'" := (Byte.x7d) (only printing). +Notation "'~'" := (Byte.x7e) (only printing). + +Global Set Printing Width 300. + +Goal False. + let cc := eval cbv in allBytes in idtac cc. +Abort. diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v index 4717759dec..b403fc120c 100644 --- a/test-suite/success/attribute_syntax.v +++ b/test-suite/success/attribute_syntax.v @@ -36,3 +36,10 @@ Check M.zed@{_}. Fail Check zed. Check M.kats@{_}. Fail Check kats. + +Export Set Foo. + +#[ export ] Set Foo. + +Fail #[ export ] Export Foo. +(* Attribute for Locality specified twice *) diff --git a/test-suite/success/search.v b/test-suite/success/search.v new file mode 100644 index 0000000000..92de43e052 --- /dev/null +++ b/test-suite/success/search.v @@ -0,0 +1,35 @@ + +(** Test of the different syntaxes of Search *) + +Search plus. +Search plus mult. +Search "plus_n". +Search plus "plus_n". +Search "*". +Search "*" "+". + +Search plus inside Peano. +Search plus mult inside Peano. +Search "plus_n" inside Peano. +Search plus "plus_n" inside Peano. +Search "*" inside Peano. +Search "*" "+" inside Peano. + +Search plus outside Peano Logic. +Search plus mult outside Peano Logic. +Search "plus_n" outside Peano Logic. +Search plus "plus_n" outside Peano Logic. +Search "*" outside Peano Logic. +Search "*" "+" outside Peano Logic. + +Search -"*" "+" outside Logic. +Search -"*"%nat "+"%nat outside Logic. + + +(** The example in the Reference Manual *) + +Require Import ZArith. + +Search Z.mul Z.add "distr". +Search "+"%Z "*"%Z "distr" -positive -Prop. +Search (?x * _ + ?x * _)%Z outside OmegaLemmas. diff --git a/test-suite/success/searchabout.v b/test-suite/success/searchabout.v deleted file mode 100644 index 9edfd82556..0000000000 --- a/test-suite/success/searchabout.v +++ /dev/null @@ -1,60 +0,0 @@ - -(** Test of the different syntaxes of SearchAbout, in particular - with and without the [ ... ] delimiters *) - -SearchAbout plus. -SearchAbout plus mult. -SearchAbout "plus_n". -SearchAbout plus "plus_n". -SearchAbout "*". -SearchAbout "*" "+". - -SearchAbout plus inside Peano. -SearchAbout plus mult inside Peano. -SearchAbout "plus_n" inside Peano. -SearchAbout plus "plus_n" inside Peano. -SearchAbout "*" inside Peano. -SearchAbout "*" "+" inside Peano. - -SearchAbout plus outside Peano Logic. -SearchAbout plus mult outside Peano Logic. -SearchAbout "plus_n" outside Peano Logic. -SearchAbout plus "plus_n" outside Peano Logic. -SearchAbout "*" outside Peano Logic. -SearchAbout "*" "+" outside Peano Logic. - -SearchAbout -"*" "+" outside Logic. -SearchAbout -"*"%nat "+"%nat outside Logic. - -SearchAbout [plus]. -SearchAbout [plus mult]. -SearchAbout ["plus_n"]. -SearchAbout [plus "plus_n"]. -SearchAbout ["*"]. -SearchAbout ["*" "+"]. - -SearchAbout [plus] inside Peano. -SearchAbout [plus mult] inside Peano. -SearchAbout ["plus_n"] inside Peano. -SearchAbout [plus "plus_n"] inside Peano. -SearchAbout ["*"] inside Peano. -SearchAbout ["*" "+"] inside Peano. - -SearchAbout [plus] outside Peano Logic. -SearchAbout [plus mult] outside Peano Logic. -SearchAbout ["plus_n"] outside Peano Logic. -SearchAbout [plus "plus_n"] outside Peano Logic. -SearchAbout ["*"] outside Peano Logic. -SearchAbout ["*" "+"] outside Peano Logic. - -SearchAbout [-"*" "+"] outside Logic. -SearchAbout [-"*"%nat "+"%nat] outside Logic. - - -(** The example in the Reference Manual *) - -Require Import ZArith. - -SearchAbout Z.mul Z.add "distr". -SearchAbout "+"%Z "*"%Z "distr" -positive -Prop. -SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas. |