diff options
Diffstat (limited to 'test-suite')
48 files changed, 865 insertions, 106 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 245c717d42..2a2f62e23f 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -46,7 +46,11 @@ BIN := $(ROOT)/bin/ COQLIB?= ifeq ($(COQLIB),) + ifeq ($(LOCAL),true) COQLIB := $(shell ocaml ocaml_pwd.ml ..) + else + COQLIB := $(shell ocaml ocaml_pwd.ml $(COQLIBINSTALL)) + endif endif endif # exists ../_build export COQLIB @@ -320,7 +324,7 @@ unit-tests: $(UNIT_LOGFILES) # Build executable, run it to generate log file unit-tests/%.ml.log: unit-tests/%.ml unit-tests/src/$(UNIT_LINK) $(SHOW) 'TEST $<' - $(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.toplevel,ounit2 \ + $(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq-core.toplevel,ounit2 \ -I unit-tests/src $(UNIT_LINK) $< -o $<.test; $(HIDE)./$<.test diff --git a/test-suite/bugs/closed/bug_13732.v b/test-suite/bugs/closed/bug_13732.v new file mode 100644 index 0000000000..24840abdf6 --- /dev/null +++ b/test-suite/bugs/closed/bug_13732.v @@ -0,0 +1,16 @@ +Module Sort. + Set Printing Universes. + + Implicit Types TT : Type. + + Check fun TT => nat. +End Sort. + +Module Ref. + Set Universe Polymorphism. + + Axiom tele : Type. + + Implicit Types TT : tele. + Check fun TT => nat. +End Ref. diff --git a/test-suite/bugs/closed/bug_13755.v b/test-suite/bugs/closed/bug_13755.v new file mode 100644 index 0000000000..cc25157b9b --- /dev/null +++ b/test-suite/bugs/closed/bug_13755.v @@ -0,0 +1,5 @@ +Module M1. +Lemma t1 : True. +Fail End M1. +Proof. exact I. Qed. +End M1. diff --git a/test-suite/bugs/closed/bug_4836.v b/test-suite/bugs/closed/bug_4836.v index 9aefb10172..62d39619b0 100644 --- a/test-suite/bugs/closed/bug_4836.v +++ b/test-suite/bugs/closed/bug_4836.v @@ -1 +1 @@ -(* -*- coq-prog-args: ("bugs/closed/PLACEHOLDER.v") -*- *) +(* Placeholder file for directory / file test *) diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/007-no-output-sync/time-of-build.log.in b/test-suite/coq-makefile/timing/precomputed-time-tests/007-no-output-sync/time-of-build.log.in index 47d0e09e1a..258eb04271 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/007-no-output-sync/time-of-build.log.in +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/007-no-output-sync/time-of-build.log.in @@ -744,7 +744,7 @@ CONTRIBUTING.md CREDITS INSTALL.md LICENSE -META.coq.in +META.coq-core.in Makefile Makefile.build Makefile.checker @@ -5626,4 +5626,4 @@ ValueError: too many values to unpack Makefile.ci:90: recipe for target 'ci-metacoq' failed make: *** [ci-metacoq] Error 1 section_end:1598965182:build_script
[0Ksection_start:1598965182:after_script
[0Ksection_end:1598965184:after_script
[0Ksection_start:1598965184:upload_artifacts_on_failure
[0Ksection_end:1598965189:upload_artifacts_on_failure
[0K[31;1mERROR: Job failed: exit code 1 -[0;m
\ No newline at end of file +[0;m diff --git a/test-suite/dune b/test-suite/dune index 1864153021..09597fc864 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -35,7 +35,8 @@ ; For the changelog test ../config/coq_config.py (source_tree doc/changelog) - (package coq) + (package coq-core) + (package coq-stdlib) ; For fake_ide (package coqide-server) (source_tree .)) diff --git a/test-suite/micromega/bug_13794.v b/test-suite/micromega/bug_13794.v new file mode 100644 index 0000000000..5e303a0b7f --- /dev/null +++ b/test-suite/micromega/bug_13794.v @@ -0,0 +1,39 @@ +From Coq Require Import Lia ZArith.ZArith NArith.NArith. +Unset Nia Cache. + +Open Scope N_scope. + + +Lemma over (n0 n1 n2 n3 n4 n5 n6 : N) + (e0 : 1 + 8 * n0 = n1 * n1 + n2) + (e1 : n1 - 1 = 2 * n3 + n4) + (e2 : n3 * (1 + n3) = 2 * n5) + (e3 : n2 + 2 * n4 * n1 - n4 = 8 * n6) + (o0 : n4 = 0 \/ n4 = 1) : + n6 = n0 - n5. +Proof. + Time nia. +Qed. + +Lemma over2 (n0 n1 n2 n3 n4 n5 n6 : N) + (e0 : 1 + 8 * n0 = n1 * n1 + n2) + (e1 : n1 + 1 = 2 * n3 + n4) + (e2 : n3 * (1 + n3) = 2 * n5) + (e3 : n2 + 2 * n4 * n1 + n4 = 8 * n6) + (o0 : n4 = 0) : + n6 = n0 + n5. +Proof. + Fail nia. +Abort. + +Open Scope Z_scope. + +Lemma over3 (n1 n2 n3 n4 n5 : Z) + (e : 0 <= n1 /\ 0 <= n2 /\ 0 <= n3 /\ 0 <= n4 + /\ 0 <= n5) + (e1 : n1 + 1 = 20 * n3 + n4) + (e3 : n2 + 2 * n4 * n1 + n4 = 8 * n5) : + n5 = 0. +Proof. +Time Fail nia. +Abort. diff --git a/test-suite/misc/coq_environment.sh b/test-suite/misc/coq_environment.sh index 667d11f89e..6f7b11c8f1 100755 --- a/test-suite/misc/coq_environment.sh +++ b/test-suite/misc/coq_environment.sh @@ -16,7 +16,7 @@ EOT cp $BIN/coqc . cp $BIN/coq_makefile . mkdir -p overridden/tools/ -cp $COQLIB/tools/CoqMakefile.in overridden/tools/ +cp $COQLIB/tools/CoqMakefile.in overridden/tools/ || cp $COQLIB/../coq-core/tools/CoqMakefile.in overridden/tools/ unset COQLIB N=`./coqc -config | grep COQLIB | grep /overridden | wc -l` diff --git a/test-suite/misc/coqtop_print-mod-uid.sh b/test-suite/misc/coqtop_print-mod-uid.sh new file mode 100755 index 0000000000..db1df4bb4b --- /dev/null +++ b/test-suite/misc/coqtop_print-mod-uid.sh @@ -0,0 +1,6 @@ +#!/usr/bin/env bash + +export COQBIN=$BIN +export PATH=$COQBIN:$PATH + +[ "$(coqtop -print-mod-uid prerequisite/admit.vo)" = "prerequisite/.coq-native/NTestSuite_admit" ] diff --git a/test-suite/misc/non-marshalable-state.sh b/test-suite/misc/non-marshalable-state.sh new file mode 100755 index 0000000000..eef7786ebc --- /dev/null +++ b/test-suite/misc/non-marshalable-state.sh @@ -0,0 +1,30 @@ +#!/usr/bin/env bash + +set -e + +export COQBIN=$BIN +export PATH=$COQBIN:$PATH + +cd misc/non-marshalable-state/ + +coq_makefile -f _CoqProject -o Makefile + +make clean + +make src/evil_plugin.cmxs +make src/good_plugin.cmxs + +RC=1 +# must fail +coqc -async-proofs on -I src -Q theories Marshal theories/evil.v 2> log1 1>&2 || RC=0 +# for this reason +grep -q 'Marshalling error' log1 || RC=1 + +# must work +coqc -async-proofs off -I src -Q theories Marshal theories/evil.v + +# must work +coqc -async-proofs on -I src -Q theories Marshal theories/good.v + + +exit $RC diff --git a/test-suite/misc/non-marshalable-state/_CoqProject b/test-suite/misc/non-marshalable-state/_CoqProject new file mode 100644 index 0000000000..09e68d866c --- /dev/null +++ b/test-suite/misc/non-marshalable-state/_CoqProject @@ -0,0 +1,9 @@ +-Q theories Marshal +-I src + +src/evil.mlg +src/good.mlg +src/evil_plugin.mlpack +src/good_plugin.mlpack +theories/evil.v +theories/good.v diff --git a/test-suite/misc/non-marshalable-state/src/evil.mlg b/test-suite/misc/non-marshalable-state/src/evil.mlg new file mode 100644 index 0000000000..59b2b5a8ac --- /dev/null +++ b/test-suite/misc/non-marshalable-state/src/evil.mlg @@ -0,0 +1,15 @@ +DECLARE PLUGIN "evil_plugin" + +{ + +let state = Summary.ref + ~name:"elpi-compiler-cache" + None + +} + +VERNAC COMMAND EXTEND magic CLASSIFIED AS SIDEFF +| [ "magic" ] -> { + state := Some (fun () -> ()) +} +END diff --git a/test-suite/misc/non-marshalable-state/src/evil_plugin.mlpack b/test-suite/misc/non-marshalable-state/src/evil_plugin.mlpack new file mode 100644 index 0000000000..6382aa69e1 --- /dev/null +++ b/test-suite/misc/non-marshalable-state/src/evil_plugin.mlpack @@ -0,0 +1 @@ +Evil diff --git a/test-suite/misc/non-marshalable-state/src/good.mlg b/test-suite/misc/non-marshalable-state/src/good.mlg new file mode 100644 index 0000000000..c6b9cbefd5 --- /dev/null +++ b/test-suite/misc/non-marshalable-state/src/good.mlg @@ -0,0 +1,16 @@ +DECLARE PLUGIN "good_plugin" + +{ + +let state = Summary.Local.ref + ~name:"elpi-compiler-cache" + None + +} + +VERNAC COMMAND EXTEND magic CLASSIFIED AS SIDEFF +| [ "magic" ] -> { + let open Summary.Local in + state := Some (fun () -> ()) +} +END diff --git a/test-suite/misc/non-marshalable-state/src/good_plugin.mlpack b/test-suite/misc/non-marshalable-state/src/good_plugin.mlpack new file mode 100644 index 0000000000..cd9dd73b78 --- /dev/null +++ b/test-suite/misc/non-marshalable-state/src/good_plugin.mlpack @@ -0,0 +1 @@ +Good diff --git a/test-suite/misc/non-marshalable-state/theories/evil.v b/test-suite/misc/non-marshalable-state/theories/evil.v new file mode 100644 index 0000000000..661482a975 --- /dev/null +++ b/test-suite/misc/non-marshalable-state/theories/evil.v @@ -0,0 +1,5 @@ +Declare ML Module "evil_plugin". + +magic. + +Lemma x : True. Proof. trivial. Qed. diff --git a/test-suite/misc/non-marshalable-state/theories/good.v b/test-suite/misc/non-marshalable-state/theories/good.v new file mode 100644 index 0000000000..eab9a043e1 --- /dev/null +++ b/test-suite/misc/non-marshalable-state/theories/good.v @@ -0,0 +1,5 @@ +Declare ML Module "good_plugin". + +magic. + +Lemma x : True. Proof. trivial. Qed. diff --git a/test-suite/output/DebugFlags.out b/test-suite/output/DebugFlags.out new file mode 100644 index 0000000000..0385413937 --- /dev/null +++ b/test-suite/output/DebugFlags.out @@ -0,0 +1,44 @@ +File "stdin", line 1, characters 0-16: +Warning: There is no debug flag "cbn". [unknown-debug-flag,option] +Debug: [RAKAM] <<forall A : Type, A -> A -> Prop|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<forall A : Type, A -> A -> Prop|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<?A -> ?A -> Prop|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<?A -> ?A -> Prop|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> Prop|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> Prop|>> +Debug: [RAKAM] <><><><><> +2 + 3 = 0 + : Prop diff --git a/test-suite/output/DebugFlags.v b/test-suite/output/DebugFlags.v new file mode 100644 index 0000000000..32c0f2d24b --- /dev/null +++ b/test-suite/output/DebugFlags.v @@ -0,0 +1,5 @@ +Set Debug "cbn". + +Set Debug "RAKAM". + +Check 2 + 3 = 0. diff --git a/test-suite/bugs/closed/PLACEHOLDER.v b/test-suite/output/Function.out index e69de29bb2..e69de29bb2 100644 --- a/test-suite/bugs/closed/PLACEHOLDER.v +++ b/test-suite/output/Function.out diff --git a/test-suite/output/Function.v b/test-suite/output/Function.v new file mode 100644 index 0000000000..b3e2a93895 --- /dev/null +++ b/test-suite/output/Function.v @@ -0,0 +1,31 @@ +Require Import FunInd List. + +(* Explanations: This kind of pattern matching displays a legitimate + unused variable warning in v8.13. + +Fixpoint f (l:list nat) : nat := + match l with + | nil => O + | S n :: nil => 1 + | x :: l' => f l' + end. +*) + +(* In v8.13 the same code with "Function" generates a lot more + warnings about variables created automatically by Function. These + are not legitimate. PR #13776 (post v8.13) removes all warnings + about pattern matching variables (and non truly recursive fixpoint) + for "Function". So this should not generate any warning. Note that + this PR removes also the legitimate warnings. It would be better if + this test generate the same warning as the Fixpoint above. This + test would then need to be updated. *) + +(* Ensuring the warning is a warning. *) +Set Warnings "matching-variable". +(* But no warning generated here. *) +Function f (l:list nat) : nat := + match l with + | nil => O + | S n :: nil => 1 + | n :: l' => f l' + end. diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out index 7ca4de1e46..96af456891 100644 --- a/test-suite/output/Int63Syntax.out +++ b/test-suite/output/Int63Syntax.out @@ -15,9 +15,9 @@ 427 : int The command has indeed failed with message: -Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int +Cannot interpret this number as a value of type int The command has indeed failed with message: -Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int +Cannot interpret this number as a value of type int 0 : int 0 @@ -33,9 +33,11 @@ The reference x was not found in the current environment. add 2 2 : int The command has indeed failed with message: -int63 are only non-negative numbers. +Cannot interpret this number as a value of type int The command has indeed failed with message: overflow in int63 literal: 9223372036854775808 +0x1 + : int 2 : nat 2%int63 diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v index 50910264f2..be0ee701af 100644 --- a/test-suite/output/Int63Syntax.v +++ b/test-suite/output/Int63Syntax.v @@ -20,6 +20,11 @@ Fail Check 0x. Check (PrimInt63.add 2 2). Fail Check -1. Fail Check 9223372036854775808. + +Set Printing All. +Check 1%int63. +Unset Printing All. + Open Scope nat_scope. Check 2. (* : nat *) Check 2%int63. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 3477a293e3..0b18981f4e 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -77,18 +77,18 @@ fun x : nat => [x] : nat -> nat ∀ x : nat, x = x : Prop -File "stdin", line 184, characters 0-160: +File "stdin", line 187, characters 0-160: Warning: Notation "∀ _ .. _ , _" was already defined with a different format in scope type_scope. [notation-incompatible-format,parsing] ∀x : nat,x = x : Prop -File "stdin", line 197, characters 0-60: +File "stdin", line 200, characters 0-60: Warning: Notation "_ %%% _" was already defined with a different format. [notation-incompatible-format,parsing] -File "stdin", line 201, characters 0-64: +File "stdin", line 204, characters 0-64: Warning: Notation "_ %%% _" was already defined with a different format. [notation-incompatible-format,parsing] -File "stdin", line 206, characters 0-62: +File "stdin", line 209, characters 0-62: Warning: Lonely notation "_ %%%% _" was already defined with a different format. [notation-incompatible-format,parsing] 3 %% 4 @@ -97,10 +97,10 @@ format. [notation-incompatible-format,parsing] : nat 3 %% 4 : nat -File "stdin", line 234, characters 0-61: +File "stdin", line 237, characters 0-61: Warning: The format modifier is irrelevant for only parsing rules. [irrelevant-format-only-parsing,parsing] -File "stdin", line 238, characters 0-63: +File "stdin", line 241, characters 0-63: Warning: The only parsing modifier has no effect in Reserved Notation. [irrelevant-reserved-notation-only-parsing,parsing] fun x : nat => U (S x) @@ -111,7 +111,7 @@ fun x : nat => V x : forall x : nat, nat * (?T -> ?T) where ?T : [x : nat x0 : ?T |- Type] (x0 cannot be used) -File "stdin", line 255, characters 0-30: +File "stdin", line 258, characters 0-30: Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing] 0 :=: 0 : Prop diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index ebad12af88..a5ec92fe3c 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -103,7 +103,10 @@ Module NumberNotations. Delimit Scope test17_scope with test17. Local Set Primitive Projections. Record myint63 := of_int { to_int : int }. - Number Notation myint63 of_int to_int : test17_scope. + Definition parse x := + match x with Pos x => Some (of_int x) | Neg _ => None end. + Definition print x := Pos (to_int x). + Number Notation myint63 parse print : test17_scope. Check let v := 0%test17 in v : myint63. End Test17. End NumberNotations. diff --git a/test-suite/output/NumberNotations.out b/test-suite/output/NumberNotations.out index 60682edec8..df9b39389c 100644 --- a/test-suite/output/NumberNotations.out +++ b/test-suite/output/NumberNotations.out @@ -260,28 +260,28 @@ The command has indeed failed with message: add is not a constructor of an inductive type. The command has indeed failed with message: Missing mapping for constructor Iempty. -File "stdin", line 574, characters 56-61: +File "stdin", line 577, characters 56-61: Warning: Type of I'sum seems incompatible with the type of sum. Expected type is: (I' -> I' -> I') instead of (I -> I' -> I'). This might yield ill typed terms when using the notation. [via-type-mismatch,numbers] -File "stdin", line 579, characters 32-33: +File "stdin", line 582, characters 32-33: Warning: I was already mapped to Set, mapping it also to nat might yield ill typed terms when using the notation. [via-type-remapping,numbers] -File "stdin", line 579, characters 37-42: +File "stdin", line 582, characters 37-42: Warning: Type of Iunit seems incompatible with the type of O. Expected type is: I instead of I. This might yield ill typed terms when using the notation. [via-type-mismatch,numbers] The command has indeed failed with message: 'via' and 'abstract' cannot be used together. -File "stdin", line 659, characters 21-23: +File "stdin", line 662, characters 21-23: Warning: Type of I1 seems incompatible with the type of Fin.F1. Expected type is: (nat -> I) instead of I. This might yield ill typed terms when using the notation. [via-type-mismatch,numbers] -File "stdin", line 659, characters 35-37: +File "stdin", line 662, characters 35-37: Warning: Type of IS seems incompatible with the type of Fin.FS. Expected type is: (nat -> I -> I) instead of (I -> I). This might yield ill typed terms when using the notation. diff --git a/test-suite/output/NumberNotations.v b/test-suite/output/NumberNotations.v index 718da13500..85400c2fd4 100644 --- a/test-suite/output/NumberNotations.v +++ b/test-suite/output/NumberNotations.v @@ -328,7 +328,10 @@ Module Test17. Delimit Scope test17_scope with test17. Local Set Primitive Projections. Record myint63 := of_int { to_int : int }. - Number Notation myint63 of_int to_int : test17_scope. + Definition parse x := + match x with Pos x => Some (of_int x) | Neg _ => None end. + Definition print x := Pos (to_int x). + Number Notation myint63 parse print : test17_scope. Check let v := 0%test17 in v : myint63. End Test17. diff --git a/test-suite/output/SearchHead.v b/test-suite/output/SearchHead.v deleted file mode 100644 index 2ee8a0d184..0000000000 --- a/test-suite/output/SearchHead.v +++ /dev/null @@ -1,19 +0,0 @@ -(* Some tests of the Search command *) - -SearchHead le. (* app nodes *) -SearchHead bool. (* no apps *) -SearchHead (@eq nat). (* complex pattern *) - -Definition newdef := fun x:nat => x = x. - -Goal forall n:nat, newdef n -> False. - intros n h. - SearchHead newdef. (* search hypothesis *) -Abort. - - -Goal forall n (P:nat -> Prop), P n -> False. - intros n P h. - SearchHead P. (* search hypothesis also for patterns *) -Abort. - diff --git a/test-suite/output/SearchHead.out b/test-suite/output/Search_headconcl.out index 2f0d854ac6..24e2ee76af 100644 --- a/test-suite/output/SearchHead.out +++ b/test-suite/output/Search_headconcl.out @@ -1,17 +1,9 @@ -File "stdin", line 3, characters 0-14: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] le_n: forall n : nat, n <= n le_0_n: forall n : nat, 0 <= n le_S: forall n m : nat, n <= m -> n <= S m le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m le_n_S: forall n m : nat, n <= m -> S n <= S m le_S_n: forall n m : nat, S n <= S m -> n <= m -File "stdin", line 4, characters 0-16: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] false: bool true: bool negb: bool -> bool @@ -35,10 +27,6 @@ Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool Decimal.int_beq: Decimal.int -> Decimal.int -> bool Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool -File "stdin", line 5, characters 0-21: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] mult_n_O: forall n : nat, 0 = n * 0 plus_O_n: forall n : nat, 0 + n = n plus_n_O: forall n : nat, n = n + 0 @@ -57,13 +45,5 @@ f_equal2_plus: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 f_equal2_mult: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 -File "stdin", line 11, characters 2-20: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] h: newdef n -File "stdin", line 17, characters 2-15: -Warning: -SearchHead is deprecated. Use the headconcl: clause of Search instead. -[deprecated-searchhead,deprecated] h: P n diff --git a/test-suite/output/Search_headconcl.v b/test-suite/output/Search_headconcl.v new file mode 100644 index 0000000000..8b168dcd25 --- /dev/null +++ b/test-suite/output/Search_headconcl.v @@ -0,0 +1,18 @@ +(* Some tests of the Search command *) + +Search headconcl: le. (* app nodes *) +Search headconcl: bool. (* no apps *) +Search headconcl: (@eq nat). (* complex pattern *) + +Definition newdef := fun x:nat => x = x. + +Goal forall n:nat, newdef n -> False. + intros n h. + Search headconcl: newdef. (* search hypothesis *) +Abort. + + +Goal forall n (P:nat -> Prop), P n -> False. + intros n P h. + Search headconcl: P. (* search hypothesis also for patterns *) +Abort. diff --git a/test-suite/output/Sint63Syntax.out b/test-suite/output/Sint63Syntax.out new file mode 100644 index 0000000000..db14658307 --- /dev/null +++ b/test-suite/output/Sint63Syntax.out @@ -0,0 +1,66 @@ +2%sint63 + : int +2 + : int +-3 + : int +4611686018427387903 + : int +-4611686018427387904 + : int +427 + : int +427 + : int +427 + : int +427 + : int +427 + : int +The command has indeed failed with message: +Cannot interpret this number as a value of type int +The command has indeed failed with message: +Cannot interpret this number as a value of type int +0 + : int +0 + : int +The command has indeed failed with message: +The reference xg was not found in the current environment. +The command has indeed failed with message: +The reference xG was not found in the current environment. +The command has indeed failed with message: +The reference x1 was not found in the current environment. +The command has indeed failed with message: +The reference x was not found in the current environment. +2 + 2 + : int +The command has indeed failed with message: +Cannot interpret this number as a value of type int +The command has indeed failed with message: +Cannot interpret this number as a value of type int +0x1%int63 + : int +0x7fffffffffffffff%int63 + : int +2 + : nat +2%sint63 + : int +t = 2%si63 + : int +t = 2%si63 + : int +2 + : nat +2 + : int +(2 + 2)%sint63 + : int +2 + 2 + : int + = 4 + : int + = 37151199385380486 + : int diff --git a/test-suite/output/Sint63Syntax.v b/test-suite/output/Sint63Syntax.v new file mode 100644 index 0000000000..b9ed596537 --- /dev/null +++ b/test-suite/output/Sint63Syntax.v @@ -0,0 +1,49 @@ +Require Import Sint63. + +Check 2%sint63. +Open Scope sint63_scope. +Check 2. +Check -3. +Check 4611686018427387903. +Check -4611686018427387904. +Check 0x1ab. +Check 0X1ab. +Check 0x1Ab. +Check 0x1aB. +Check 0x1AB. +Fail Check 0x1ap5. (* exponents not implemented (yet?) *) +Fail Check 0x1aP5. +Check 0x0. +Check 0x000. +Fail Check 0xg. +Fail Check 0xG. +Fail Check 00x1. +Fail Check 0x. +Check (PrimInt63.add 2 2). +Fail Check 4611686018427387904. +Fail Check -4611686018427387905. + +Set Printing All. +Check 1%sint63. +Check (-1)%sint63. +Unset Printing All. + +Open Scope nat_scope. +Check 2. (* : nat *) +Check 2%sint63. +Delimit Scope sint63_scope with si63. +Definition t := 2%sint63. +Print t. +Delimit Scope nat_scope with sint63. +Print t. +Check 2. +Close Scope nat_scope. +Check 2. +Close Scope sint63_scope. +Delimit Scope sint63_scope with sint63. + +Check (2 + 2)%sint63. +Open Scope sint63_scope. +Check (2+2). +Eval vm_compute in 2+2. +Eval vm_compute in 65675757 * 565675998. diff --git a/test-suite/output/bug_13821_native_command_line_warn.out b/test-suite/output/bug_13821_native_command_line_warn.out new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/test-suite/output/bug_13821_native_command_line_warn.out diff --git a/test-suite/output/bug_13821_native_command_line_warn.v b/test-suite/output/bug_13821_native_command_line_warn.v new file mode 100644 index 0000000000..a28210b6c2 --- /dev/null +++ b/test-suite/output/bug_13821_native_command_line_warn.v @@ -0,0 +1 @@ +(* -*- coq-prog-args: ("-w" "-native-compiler-disabled" "-native-compiler" "ondemand"); -*- *) diff --git a/test-suite/primitive/sint63/add.v b/test-suite/primitive/sint63/add.v new file mode 100644 index 0000000000..dcafd64181 --- /dev/null +++ b/test-suite/primitive/sint63/add.v @@ -0,0 +1,25 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 2 + 3 = 5). +Check (eq_refl 5 <: 2 + 3 = 5). +Check (eq_refl 5 <<: 2 + 3 = 5). +Definition compute1 := Eval compute in 2 + 3. +Check (eq_refl compute1 : 5 = 5). + +Check (eq_refl : 4611686018427387903 + 1 = -4611686018427387904). +Check (eq_refl (-4611686018427387904) <: + 4611686018427387903 + 1 = -4611686018427387904). +Check (eq_refl (-4611686018427387904) <<: + 4611686018427387903 + 1 = -4611686018427387904). +Definition compute2 := Eval compute in 4611686018427387903 + 1. +Check (eq_refl compute2 : -4611686018427387904 = -4611686018427387904). + +Check (eq_refl : 2 - 3 = -1). +Check (eq_refl (-1) <: 2 - 3 = -1). +Check (eq_refl (-1) <<: 2 - 3 = -1). +Definition compute3 := Eval compute in 2 - 3. +Check (eq_refl compute3 : -1 = -1). diff --git a/test-suite/primitive/sint63/asr.v b/test-suite/primitive/sint63/asr.v new file mode 100644 index 0000000000..4524ae4e6f --- /dev/null +++ b/test-suite/primitive/sint63/asr.v @@ -0,0 +1,41 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : (-2305843009213693952) >> 61 = -1). +Check (eq_refl (-1) <: (-2305843009213693952) >> 61 = -1). +Check (eq_refl (-1) <<: (-2305843009213693952) >> 61 = -1). +Definition compute1 := Eval compute in (-2305843009213693952) >> 61. +Check (eq_refl compute1 : -1 = -1). + +Check (eq_refl : 2305843009213693952 >> 62 = 0). +Check (eq_refl 0 <: 2305843009213693952 >> 62 = 0). +Check (eq_refl 0 <<: 2305843009213693952 >> 62 = 0). +Definition compute2 := Eval compute in 2305843009213693952 >> 62. +Check (eq_refl compute2 : 0 = 0). + +Check (eq_refl : 4611686018427387903 >> 63 = 0). +Check (eq_refl 0 <: 4611686018427387903 >> 63 = 0). +Check (eq_refl 0 <<: 4611686018427387903 >> 63 = 0). +Definition compute3 := Eval compute in 4611686018427387903 >> 63. +Check (eq_refl compute3 : 0 = 0). + +Check (eq_refl : (-1) >> 1 = -1). +Check (eq_refl (-1) <: (-1) >> 1 = -1). +Check (eq_refl (-1) <<: (-1) >> 1 = -1). +Definition compute4 := Eval compute in (-1) >> 1. +Check (eq_refl compute4 : -1 = -1). + +Check (eq_refl : (-1) >> (-1) = 0). +Check (eq_refl 0 <: (-1) >> (-1) = 0). +Check (eq_refl 0 <<: (-1) >> (-1) = 0). +Definition compute5 := Eval compute in (-1) >> (-1). +Check (eq_refl compute5 : 0 = 0). + +Check (eq_refl : 73 >> (-2) = 0). +Check (eq_refl 0 <: 73 >> (-2) = 0). +Check (eq_refl 0 <<: 73 >> (-2) = 0). +Definition compute6 := Eval compute in 73 >> (-2). +Check (eq_refl compute6 : 0 = 0). diff --git a/test-suite/primitive/sint63/compare.v b/test-suite/primitive/sint63/compare.v new file mode 100644 index 0000000000..7a9882f1c8 --- /dev/null +++ b/test-suite/primitive/sint63/compare.v @@ -0,0 +1,36 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 1 ?= 1 = Eq). +Check (eq_refl Eq <: 1 ?= 1 = Eq). +Check (eq_refl Eq <<: 1 ?= 1 = Eq). +Definition compute1 := Eval compute in 1 ?= 1. +Check (eq_refl compute1 : Eq = Eq). + +Check (eq_refl : 1 ?= 2 = Lt). +Check (eq_refl Lt <: 1 ?= 2 = Lt). +Check (eq_refl Lt <<: 1 ?= 2 = Lt). +Definition compute2 := Eval compute in 1 ?= 2. +Check (eq_refl compute2 : Lt = Lt). + +Check (eq_refl : 4611686018427387903 ?= 0 = Gt). +Check (eq_refl Gt <: 4611686018427387903 ?= 0 = Gt). +Check (eq_refl Gt <<: 4611686018427387903 ?= 0 = Gt). +Definition compute3 := Eval compute in 4611686018427387903 ?= 0. +Check (eq_refl compute3 : Gt = Gt). + +Check (eq_refl : -1 ?= 1 = Lt). +Check (eq_refl Lt <: -1 ?= 1 = Lt). +Check (eq_refl Lt <<: -1 ?= 1 = Lt). +Definition compute4 := Eval compute in -1 ?= 1. +Check (eq_refl compute4 : Lt = Lt). + +Check (eq_refl : 4611686018427387903 ?= -4611686018427387904 = Gt). +Check (eq_refl Gt <: 4611686018427387903 ?= -4611686018427387904 = Gt). +Check (eq_refl Gt <<: 4611686018427387903 ?= -4611686018427387904 = Gt). +Definition compute5 := + Eval compute in 4611686018427387903 ?= -4611686018427387904. +Check (eq_refl compute5 : Gt = Gt). diff --git a/test-suite/primitive/sint63/div.v b/test-suite/primitive/sint63/div.v new file mode 100644 index 0000000000..9da628ce1e --- /dev/null +++ b/test-suite/primitive/sint63/div.v @@ -0,0 +1,61 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 6 / 3 = 2). +Check (eq_refl 2 <: 6 / 3 = 2). +Check (eq_refl 2 <<: 6 / 3 = 2). +Definition compute1 := Eval compute in 6 / 3. +Check (eq_refl compute1 : 2 = 2). + +Check (eq_refl : -6 / 3 = -2). +Check (eq_refl (-2) <: -6 / 3 = -2). +Check (eq_refl (-2) <<: -6 / 3 = -2). +Definition compute2 := Eval compute in -6 / 3. +Check (eq_refl compute2 : -2 = -2). + +Check (eq_refl : 6 / -3 = -2). +Check (eq_refl (-2) <: 6 / -3 = -2). +Check (eq_refl (-2) <<: 6 / -3 = -2). +Definition compute3 := Eval compute in 6 / -3. +Check (eq_refl compute3 : -2 = -2). + +Check (eq_refl : -6 / -3 = 2). +Check (eq_refl 2 <: -6 / -3 = 2). +Check (eq_refl 2 <<: -6 / -3 = 2). +Definition compute4 := Eval compute in -6 / -3. +Check (eq_refl compute4 : 2 = 2). + +Check (eq_refl : 3 / 2 = 1). +Check (eq_refl 1 <: 3 / 2 = 1). +Check (eq_refl 1 <<: 3 / 2 = 1). +Definition compute5 := Eval compute in 3 / 2. +Check (eq_refl compute5 : 1 = 1). + +Check (eq_refl : -3 / 2 = -1). +Check (eq_refl (-1) <: -3 / 2 = -1). +Check (eq_refl (-1) <<: -3 / 2 = -1). +Definition compute6 := Eval compute in -3 / 2. +Check (eq_refl compute6 : -1 = -1). + +Check (eq_refl : 3 / -2 = -1). +Check (eq_refl (-1) <: 3 / -2 = -1). +Check (eq_refl (-1) <<: 3 / -2 = -1). +Definition compute7 := Eval compute in 3 / -2. +Check (eq_refl compute7 : -1 = -1). + +Check (eq_refl : -3 / -2 = 1). +Check (eq_refl 1 <: -3 / -2 = 1). +Check (eq_refl 1 <<: -3 / -2 = 1). +Definition compute8 := Eval compute in -3 / -2. +Check (eq_refl compute8 : 1 = 1). + +Check (eq_refl : -4611686018427387904 / -1 = -4611686018427387904). +Check (eq_refl (-4611686018427387904) <: + -4611686018427387904 / -1 = -4611686018427387904). +Check (eq_refl (-4611686018427387904) <<: + -4611686018427387904 / -1 = -4611686018427387904). +Definition compute9 := Eval compute in -4611686018427387904 / -1. +Check (eq_refl compute9 : -4611686018427387904 = -4611686018427387904). diff --git a/test-suite/primitive/sint63/eqb.v b/test-suite/primitive/sint63/eqb.v new file mode 100644 index 0000000000..4d365acf54 --- /dev/null +++ b/test-suite/primitive/sint63/eqb.v @@ -0,0 +1,17 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 1 =? 1 = true). +Check (eq_refl true <: 1 =? 1 = true). +Check (eq_refl true <<: 1 =? 1 = true). +Definition compute1 := Eval compute in 1 =? 1. +Check (eq_refl compute1 : true = true). + +Check (eq_refl : 4611686018427387903 =? 0 = false). +Check (eq_refl false <: 4611686018427387903 =? 0 = false). +Check (eq_refl false <<: 4611686018427387903 =? 0 = false). +Definition compute2 := Eval compute in 4611686018427387903 =? 0. +Check (eq_refl compute2 : false = false). diff --git a/test-suite/primitive/sint63/isint.v b/test-suite/primitive/sint63/isint.v new file mode 100644 index 0000000000..f1c9c2cfd1 --- /dev/null +++ b/test-suite/primitive/sint63/isint.v @@ -0,0 +1,50 @@ +(* This file tests the check that arithmetic operations use to know if their +arguments are ground. The various test cases correspond to possible +optimizations of these tests made by the compiler. *) +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Section test. + +Variable m n : int. + +Check (eq_refl : (fun x => x + 3) m = m + 3). +Check (eq_refl (m + 3) <: (fun x => x + 3) m = m + 3). +Check (eq_refl (m + 3) <<: (fun x => x + 3) m = m + 3). +Definition compute1 := Eval compute in (fun x => x + 3) m. +Check (eq_refl compute1 : m + 3 = m + 3). + +Check (eq_refl : (fun x => 3 + x) m = 3 + m). +Check (eq_refl (3 + m) <: (fun x => 3 + x) m = 3 + m). +Check (eq_refl (3 + m) <<: (fun x => 3 + x) m = 3 + m). +Definition compute2 := Eval compute in (fun x => 3 + x) m. +Check (eq_refl compute2 : 3 + m = 3 + m). + +Check (eq_refl : (fun x y => x + y) m n = m + n). +Check (eq_refl (m + n) <: (fun x y => x + y) m n = m + n). +Check (eq_refl (m + n) <<: (fun x y => x + y) m n = m + n). +Definition compute3 := Eval compute in (fun x y => x + y) m n. +Check (eq_refl compute3 : m + n = m + n). + +Check (eq_refl : (fun x y => x + y) 2 3 = 5). +Check (eq_refl 5 <: (fun x y => x + y) 2 3 = 5). +Check (eq_refl 5 <<: (fun x y => x + y) 2 3 = 5). +Definition compute4 := Eval compute in (fun x y => x + y) 2 3. +Check (eq_refl compute4 : 5 = 5). + +Check (eq_refl : (fun x => x + x) m = m + m). +Check (eq_refl (m + m) <: (fun x => x + x) m = m + m). +Check (eq_refl (m + m) <<: (fun x => x + x) m = m + m). +Definition compute5 := Eval compute in (fun x => x + x) m. +Check (eq_refl compute5 : m + m = m + m). + +Check (eq_refl : (fun x => x + x) 2 = 4). +Check (eq_refl 4 <: (fun x => x + x) 2 = 4). +Check (eq_refl 4 <<: (fun x => x + x) 2 = 4). +Definition compute6 := Eval compute in (fun x => x + x) 2. +Check (eq_refl compute6 : 4 = 4). + +End test. diff --git a/test-suite/primitive/sint63/leb.v b/test-suite/primitive/sint63/leb.v new file mode 100644 index 0000000000..dbe958e41d --- /dev/null +++ b/test-suite/primitive/sint63/leb.v @@ -0,0 +1,29 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 1 <=? 1 = true). +Check (eq_refl true <: 1 <=? 1 = true). +Check (eq_refl true <<: 1 <=? 1 = true). +Definition compute1 := Eval compute in 1 <=? 1. +Check (eq_refl compute1 : true = true). + +Check (eq_refl : 1 <=? 2 = true). +Check (eq_refl true <: 1 <=? 2 = true). +Check (eq_refl true <<: 1 <=? 2 = true). +Definition compute2 := Eval compute in 1 <=? 2. +Check (eq_refl compute2 : true = true). + +Check (eq_refl : 4611686018427387903 <=? 0 = false). +Check (eq_refl false <: 4611686018427387903 <=? 0 = false). +Check (eq_refl false <<: 4611686018427387903 <=? 0 = false). +Definition compute3 := Eval compute in 4611686018427387903 <=? 0. +Check (eq_refl compute3 : false = false). + +Check (eq_refl : 1 <=? -1 = false). +Check (eq_refl false <: 1 <=? -1 = false). +Check (eq_refl false <<: 1 <=? -1 = false). +Definition compute4 := Eval compute in 1 <=? -1. +Check (eq_refl compute4 : false = false). diff --git a/test-suite/primitive/sint63/lsl.v b/test-suite/primitive/sint63/lsl.v new file mode 100644 index 0000000000..082c42979a --- /dev/null +++ b/test-suite/primitive/sint63/lsl.v @@ -0,0 +1,43 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 3 << 61 = -2305843009213693952). +Check (eq_refl (-2305843009213693952) <: 3 << 61 = -2305843009213693952). +Check (eq_refl (-2305843009213693952) <<: 3 << 61 = -2305843009213693952). +Definition compute1 := Eval compute in 3 << 61. +Check (eq_refl compute1 : -2305843009213693952 = -2305843009213693952). + +Check (eq_refl : 2 << 62 = 0). +Check (eq_refl 0 <: 2 << 62 = 0). +Check (eq_refl 0 <<: 2 << 62 = 0). +Definition compute2 := Eval compute in 2 << 62. +Check (eq_refl compute2 : 0 = 0). + +Check (eq_refl : 4611686018427387903 << 63 = 0). +Check (eq_refl 0 <: 4611686018427387903 << 63 = 0). +Check (eq_refl 0 <<: 4611686018427387903 << 63 = 0). +Definition compute3 := Eval compute in 4611686018427387903 << 63. +Check (eq_refl compute3 : 0 = 0). + +Check (eq_refl : 4611686018427387903 << 62 = -4611686018427387904). +Check (eq_refl (-4611686018427387904) <: + 4611686018427387903 << 62 = -4611686018427387904). +Check (eq_refl (-4611686018427387904) <<: + 4611686018427387903 << 62 = -4611686018427387904). +Definition compute4 := Eval compute in 4611686018427387903 << 62. +Check (eq_refl compute4 : -4611686018427387904 = -4611686018427387904). + +Check (eq_refl : 1 << 62 = -4611686018427387904). +Check (eq_refl (-4611686018427387904) <: 1 << 62 = -4611686018427387904). +Check (eq_refl (-4611686018427387904) <<: 1 << 62 = -4611686018427387904). +Definition compute5 := Eval compute in 1 << 62. +Check (eq_refl compute5 : -4611686018427387904 = -4611686018427387904). + +Check (eq_refl : -1 << 1 = -2). +Check (eq_refl (-2) <: -1 << 1 = -2). +Check (eq_refl (-2) <<: -1 << 1 = -2). +Definition compute6 := Eval compute in -1 << 1. +Check (eq_refl compute6 : -2 = -2). diff --git a/test-suite/primitive/sint63/ltb.v b/test-suite/primitive/sint63/ltb.v new file mode 100644 index 0000000000..aa72e1d377 --- /dev/null +++ b/test-suite/primitive/sint63/ltb.v @@ -0,0 +1,29 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 1 <? 1 = false). +Check (eq_refl false <: 1 <? 1 = false). +Check (eq_refl false <<: 1 <? 1 = false). +Definition compute1 := Eval compute in 1 <? 1. +Check (eq_refl compute1 : false = false). + +Check (eq_refl : 1 <? 2 = true). +Check (eq_refl true <: 1 <? 2 = true). +Check (eq_refl true <<: 1 <? 2 = true). +Definition compute2 := Eval compute in 1 <? 2. +Check (eq_refl compute2 : true = true). + +Check (eq_refl : 4611686018427387903 <? 0 = false). +Check (eq_refl false <: 4611686018427387903 <? 0 = false). +Check (eq_refl false <<: 4611686018427387903 <? 0 = false). +Definition compute3 := Eval compute in 4611686018427387903 <? 0. +Check (eq_refl compute3 : false = false). + +Check (eq_refl : 1 <? -1 = false). +Check (eq_refl false <: 1 <? -1 = false). +Check (eq_refl false <<: 1 <? -1 = false). +Definition compute4 := Eval compute in 1 <? -1. +Check (eq_refl compute4 : false = false). diff --git a/test-suite/primitive/sint63/mod.v b/test-suite/primitive/sint63/mod.v new file mode 100644 index 0000000000..a4872b45f3 --- /dev/null +++ b/test-suite/primitive/sint63/mod.v @@ -0,0 +1,53 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 6 mod 3 = 0). +Check (eq_refl 0 <: 6 mod 3 = 0). +Check (eq_refl 0 <<: 6 mod 3 = 0). +Definition compute1 := Eval compute in 6 mod 3. +Check (eq_refl compute1 : 0 = 0). + +Check (eq_refl : -6 mod 3 = 0). +Check (eq_refl 0 <: -6 mod 3 = 0). +Check (eq_refl 0 <<: -6 mod 3 = 0). +Definition compute2 := Eval compute in -6 mod 3. +Check (eq_refl compute2 : 0 = 0). + +Check (eq_refl : 6 mod -3 = 0). +Check (eq_refl 0 <: 6 mod -3 = 0). +Check (eq_refl 0 <<: 6 mod -3 = 0). +Definition compute3 := Eval compute in 6 mod -3. +Check (eq_refl compute3 : 0 = 0). + +Check (eq_refl : -6 mod -3 = 0). +Check (eq_refl 0 <: -6 mod -3 = 0). +Check (eq_refl 0 <<: -6 mod -3 = 0). +Definition compute4 := Eval compute in -6 mod -3. +Check (eq_refl compute4 : 0 = 0). + +Check (eq_refl : 5 mod 3 = 2). +Check (eq_refl 2 <: 5 mod 3 = 2). +Check (eq_refl 2 <<: 5 mod 3 = 2). +Definition compute5 := Eval compute in 5 mod 3. +Check (eq_refl compute5 : 2 = 2). + +Check (eq_refl : -5 mod 3 = -2). +Check (eq_refl (-2) <: -5 mod 3 = -2). +Check (eq_refl (-2) <<: -5 mod 3 = -2). +Definition compute6 := Eval compute in -5 mod 3. +Check (eq_refl compute6 : -2 = -2). + +Check (eq_refl : 5 mod -3 = 2). +Check (eq_refl 2 <: 5 mod -3 = 2). +Check (eq_refl 2 <<: 5 mod -3 = 2). +Definition compute7 := Eval compute in 5 mod -3. +Check (eq_refl compute7 : 2 = 2). + +Check (eq_refl : -5 mod -3 = -2). +Check (eq_refl (-2) <: -5 mod -3 = -2). +Check (eq_refl (-2) <<: -5 mod -3 = -2). +Definition compute8 := Eval compute in -5 mod -3. +Check (eq_refl compute8 : -2 = -2). diff --git a/test-suite/primitive/sint63/mul.v b/test-suite/primitive/sint63/mul.v new file mode 100644 index 0000000000..f72f643083 --- /dev/null +++ b/test-suite/primitive/sint63/mul.v @@ -0,0 +1,35 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 2 * 3 = 6). +Check (eq_refl 6 <: 2 * 3 = 6). +Check (eq_refl 6 <<: 2 * 3 = 6). +Definition compute1 := Eval compute in 2 * 3. +Check (eq_refl compute1 : 6 = 6). + +Check (eq_refl : -2 * 3 = -6). +Check (eq_refl (-6) <: -2 * 3 = -6). +Check (eq_refl (-6) <<: -2 * 3 = -6). +Definition compute2 := Eval compute in -2 * 3. +Check (eq_refl compute2 : -6 = -6). + +Check (eq_refl : 2 * -3 = -6). +Check (eq_refl (-6) <: 2 * -3 = -6). +Check (eq_refl (-6) <<: 2 * -3 = -6). +Definition compute3 := Eval compute in 2 * -3. +Check (eq_refl compute3 : -6 = -6). + +Check (eq_refl : -2 * -3 = 6). +Check (eq_refl 6 <: -2 * -3 = 6). +Check (eq_refl 6 <<: -2 * -3 = 6). +Definition compute4 := Eval compute in -2 * -3. +Check (eq_refl compute4 : 6 = 6). + +Check (eq_refl : 4611686018427387903 * 2 = -2). +Check (eq_refl (-2) <: 4611686018427387903 * 2 = -2). +Check (eq_refl (-2) <<: 4611686018427387903 * 2 = -2). +Definition compute5 := Eval compute in 4611686018427387903 * 2. +Check (eq_refl compute5 : -2 = -2). diff --git a/test-suite/primitive/sint63/signed.v b/test-suite/primitive/sint63/signed.v new file mode 100644 index 0000000000..d8333a8efb --- /dev/null +++ b/test-suite/primitive/sint63/signed.v @@ -0,0 +1,18 @@ +(* This file checks that operations over sint63 are signed. *) +Require Import Sint63. + +Open Scope sint63_scope. + +(* (0-1) must be negative 1 and not the maximum integer value *) + +Check (eq_refl : 1/(0-1) = -1). +Check (eq_refl (-1) <: 1/(0-1) = -1). +Check (eq_refl (-1) <<: 1/(0-1) = -1). +Definition compute1 := Eval compute in 1/(0-1). +Check (eq_refl compute1 : -1 = -1). + +Check (eq_refl : 3 mod (0-1) = 0). +Check (eq_refl 0 <: 3 mod (0-1) = 0). +Check (eq_refl 0 <<: 3 mod (0-1) = 0). +Definition compute2 := Eval compute in 3 mod (0-1). +Check (eq_refl compute2 : 0 = 0). diff --git a/test-suite/primitive/sint63/sub.v b/test-suite/primitive/sint63/sub.v new file mode 100644 index 0000000000..8504177286 --- /dev/null +++ b/test-suite/primitive/sint63/sub.v @@ -0,0 +1,25 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 3 - 2 = 1). +Check (eq_refl 1 <: 3 - 2 = 1). +Check (eq_refl 1 <<: 3 - 2 = 1). +Definition compute1 := Eval compute in 3 - 2. +Check (eq_refl compute1 : 1 = 1). + +Check (eq_refl : 0 - 1 = -1). +Check (eq_refl (-1) <: 0 - 1 = -1). +Check (eq_refl (-1) <<: 0 - 1 = -1). +Definition compute2 := Eval compute in 0 - 1. +Check (eq_refl compute2 : -1 = -1). + +Check (eq_refl : -4611686018427387904 - 1 = 4611686018427387903). +Check (eq_refl 4611686018427387903 <: + -4611686018427387904 - 1 = 4611686018427387903). +Check (eq_refl 4611686018427387903 <<: + -4611686018427387904 - 1 = 4611686018427387903). +Definition compute3 := Eval compute in -4611686018427387904 - 1. +Check (eq_refl compute3 : 4611686018427387903 = 4611686018427387903). diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 4983ee3c0d..615350c58c 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -154,50 +154,6 @@ induction H. change (0 = z -> True) in IHrepr''. Abort. -(* Test double induction *) - -(* This was failing in 8.5 and before because of a bug in the order of - hypotheses *) - -Set Warnings "-deprecated". - -Inductive I2 : Type := - C2 : forall x:nat, x=x -> I2. -Goal forall a b:I2, a = b. -double induction a b. -Abort. - -(* This was leaving useless hypotheses in 8.5 and before because of - the same bug. This is a change of compatibility. *) - -Inductive I3 : Prop := - C3 : forall x:nat, x=x -> I3. -Goal forall a b:I3, a = b. -double induction a b. -Fail clear H. (* H should have been erased *) -Abort. - -(* This one had quantification in reverse order in 8.5 and before *) -(* This is a change of compatibility. *) - -Goal forall m n, le m n -> le n m -> n=m. -intros m n. double induction 1 2. -3:destruct 1. (* Should be "S m0 <= m0" *) -Abort. - -(* Idem *) - -Goal forall m n p q, le m n -> le p q -> n+p=m+q. -intros *. double induction 1 2. -3:clear H2. (* H2 should have been erased *) -Abort. - -(* This is unchanged *) - -Goal forall m n:nat, n=m. -double induction m n. -Abort. - (* Mentioned as part of bug #12944 *) Inductive test : Set := cons : forall (IHv : nat) (v : test), test. |