diff options
Diffstat (limited to 'test-suite')
52 files changed, 311 insertions, 408 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index e15094ccfa..5ab4cacdaf 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -169,9 +169,7 @@ summary.log: # local build, and downloadable on GitLab) report: summary.log $(HIDE)./save-logs.sh - $(HIDE)if [ -n "${TRAVIS}" ]; then echo 'travis_fold:start:coq.logs'; fi - $(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec cat '{}' ';'; fi - $(HIDE)if [ -n "${TRAVIS}" ]; then echo 'travis_fold:end:coq.logs'; fi + $(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo "travis_fold:start:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo "travis_fold:end:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';'; fi $(HIDE)if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi ####################################################################### diff --git a/test-suite/bugs/closed/2141.v b/test-suite/bugs/closed/2141.v index 941ae530fd..098a7e9e72 100644 --- a/test-suite/bugs/closed/2141.v +++ b/test-suite/bugs/closed/2141.v @@ -1,3 +1,4 @@ +Require Coq.extraction.Extraction. Require Import FSetList. Require Import OrderedTypeEx. diff --git a/test-suite/bugs/closed/3036.v b/test-suite/bugs/closed/3036.v index 451bec9b20..3b57310d6e 100644 --- a/test-suite/bugs/closed/3036.v +++ b/test-suite/bugs/closed/3036.v @@ -15,11 +15,11 @@ Definition perm := Qc. Locate Qle_bool. Definition compatibleb (p1 p2 : perm) : bool := -let p1pos := Qle_bool 00 p1 in - let p2pos := Qle_bool 00 p2 in +let p1pos := Qle_bool 0 p1 in + let p2pos := Qle_bool 0 p2 in negb ( (p1pos && p2pos) - || ((p1pos || p2pos) && (negb (Qle_bool 00 ((p1 + p2)%Qc)))))%Qc. + || ((p1pos || p2pos) && (negb (Qle_bool 0 ((p1 + p2)%Qc)))))%Qc. Definition compatible (p1 p2 : perm) := compatibleb p1 p2 = true. diff --git a/test-suite/bugs/closed/3287.v b/test-suite/bugs/closed/3287.v index 7c78131252..1b758acd73 100644 --- a/test-suite/bugs/closed/3287.v +++ b/test-suite/bugs/closed/3287.v @@ -1,3 +1,5 @@ +Require Coq.extraction.Extraction. + Module Foo. (* Definition foo := (I,I). *) Definition bar := true. diff --git a/test-suite/bugs/closed/3923.v b/test-suite/bugs/closed/3923.v index 0aa029e73d..2fb0a5439a 100644 --- a/test-suite/bugs/closed/3923.v +++ b/test-suite/bugs/closed/3923.v @@ -1,3 +1,5 @@ +Require Coq.extraction.Extraction. + Module Type TRIVIAL. Parameter t:Type. End TRIVIAL. diff --git a/test-suite/bugs/closed/4394.v b/test-suite/bugs/closed/4394.v deleted file mode 100644 index 1ad81345db..0000000000 --- a/test-suite/bugs/closed/4394.v +++ /dev/null @@ -1,19 +0,0 @@ -(* -*- coq-prog-args: ("-compat" "8.4") -*- *) - -Require Import Equality List. -Inductive Foo (I : Type -> Type) (A : Type) : Type := -| foo (B : Type) : A -> I B -> Foo I A. -Definition Family := Type -> Type. -Definition FooToo : Family -> Family := Foo. -Definition optionize (I : Type -> Type) (A : Type) := option (I A). -Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo (optionize I) A := foo (optionize I) A A. -Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }. -Definition barRec : Rec (optionize id) := {| rec := bar id |}. -Inductive Empty {T} : T -> Prop := . -Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family) nil)) (b : unit) : - Empty (a, b) -> False. -Proof. - intro e. - dependent induction e. -Qed. - diff --git a/test-suite/bugs/closed/4400.v b/test-suite/bugs/closed/4400.v deleted file mode 100644 index a89cf0cbc3..0000000000 --- a/test-suite/bugs/closed/4400.v +++ /dev/null @@ -1,19 +0,0 @@ -(* -*- coq-prog-args: ("-require" "Coq.Compat.Coq84" "-compat" "8.4") -*- *) -Require Import Coq.Lists.List Coq.Logic.JMeq Program.Equality. -Set Printing Universes. -Inductive Foo (I : Type -> Type) (A : Type) : Type := -| foo (B : Type) : A -> I B -> Foo I A. -Definition Family := Type -> Type. -Definition FooToo : Family -> Family := Foo. -Definition optionize (I : Type -> Type) (A : Type) := option (I A). -Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo(optionize I) A := foo (optionize I) A A. -Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }. -Definition barRec : Rec (optionize id) := {| rec := bar id |}. -Inductive Empty {T} : T -> Prop := . -Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family) -nil)) (b : unit) : - Empty (a, b) -> False. -Proof. - intro e. - dependent induction e. -Qed. diff --git a/test-suite/bugs/closed/4616.v b/test-suite/bugs/closed/4616.v index c862f82067..a59975dbcf 100644 --- a/test-suite/bugs/closed/4616.v +++ b/test-suite/bugs/closed/4616.v @@ -1,3 +1,5 @@ +Require Coq.extraction.Extraction. + Set Primitive Projections. Record Foo' := Foo { foo : Type }. Axiom f : forall t : Foo', foo t. diff --git a/test-suite/bugs/closed/4656.v b/test-suite/bugs/closed/4656.v deleted file mode 100644 index a59eed2c86..0000000000 --- a/test-suite/bugs/closed/4656.v +++ /dev/null @@ -1,4 +0,0 @@ -(* -*- coq-prog-args: ("-compat" "8.4") -*- *) -Goal True. - constructor 1. -Qed. diff --git a/test-suite/bugs/closed/4710.v b/test-suite/bugs/closed/4710.v index fdc8501099..5d8ca330ac 100644 --- a/test-suite/bugs/closed/4710.v +++ b/test-suite/bugs/closed/4710.v @@ -1,3 +1,5 @@ +Require Coq.extraction.Extraction. + Set Primitive Projections. Record Foo' := Foo { foo : nat }. Extraction foo. diff --git a/test-suite/bugs/closed/4727.v b/test-suite/bugs/closed/4727.v deleted file mode 100644 index cfb4548d2c..0000000000 --- a/test-suite/bugs/closed/4727.v +++ /dev/null @@ -1,10 +0,0 @@ -(* -*- coq-prog-args: ("-compat" "8.4") -*- *) -Goal forall (P : Set) (l : P) (P0 : Set) (w w0 : P0) (T : Type) (a : P * T) (o : P -> option P0), - (forall (l1 l2 : P) (w1 : P0), o l1 = Some w1 -> o l2 = Some w1 -> l1 = l2) -> - o l = Some w -> o (fst a) = Some w0 -> {w = w0} + {w <> w0} -> False. -Proof. - clear; intros ???????? inj H0 H1 H2. - destruct H2; intuition subst. - eapply inj in H1; [ | eauto ]. - progress subst. (* should succeed, used to not succeed *) -Abort. diff --git a/test-suite/bugs/closed/4733.v b/test-suite/bugs/closed/4733.v deleted file mode 100644 index a90abd71cf..0000000000 --- a/test-suite/bugs/closed/4733.v +++ /dev/null @@ -1,52 +0,0 @@ -(* -*- coq-prog-args: ("-compat" "8.4") -*- *) -(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5. If they use*) -Require Import Coq.Lists.List. -Require Import Coq.Vectors.Vector. -Import ListNotations. -Import VectorNotations. -Set Implicit Arguments. -Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T). -Arguments mynil {_}, _. - -Delimit Scope mylist_scope with mylist. -Bind Scope mylist_scope with mylist. -Delimit Scope vector_scope with vector. - -Notation " [ ] " := mynil (format "[ ]") : mylist_scope. -Notation " [ x ] " := (mycons x mynil) : mylist_scope. -Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope. - -(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4. There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *) -Check [ ]%mylist : mylist _. -Check [ ]%list : list _. -Check []%vector : Vector.t _ _. -Check [ _ ]%mylist : mylist _. -Check [ _ ]%list : list _. -Check [ _ ]%vector : Vector.t _ _. -Check [ _ ; _ ]%list : list _. -Check [ _ ; _ ]%vector : Vector.t _ _. -Check [ _ ; _ ]%mylist : mylist _. -Check [ _ ; _ ; _ ]%list : list _. -Check [ _ ; _ ; _ ]%vector : Vector.t _ _. -Check [ _ ; _ ; _ ]%mylist : mylist _. -Check [ _ ; _ ; _ ; _ ]%list : list _. -Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. -Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. - -Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope. -(* Now these all work, but not so in 8.4. If we get the ability to remove notations, this section can also just be removed. *) -Check [ ]%mylist : mylist _. -Check [ ]%list : list _. -Check []%vector : Vector.t _ _. -Check [ _ ]%mylist : mylist _. -Check [ _ ]%list : list _. -Check [ _ ]%vector : Vector.t _ _. -Check [ _ ; _ ]%list : list _. -Check [ _ ; _ ]%vector : Vector.t _ _. -Check [ _ ; _ ]%mylist : mylist _. -Check [ _ ; _ ; _ ]%list : list _. -Check [ _ ; _ ; _ ]%vector : Vector.t _ _. -Check [ _ ; _ ; _ ]%mylist : mylist _. -Check [ _ ; _ ; _ ; _ ]%list : list _. -Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. -Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. diff --git a/test-suite/bugs/closed/5372.v b/test-suite/bugs/closed/5372.v index 2dc78d4c7f..e60244cd1d 100644 --- a/test-suite/bugs/closed/5372.v +++ b/test-suite/bugs/closed/5372.v @@ -1,4 +1,5 @@ (* coq bug 5372: https://coq.inria.fr/bugs/show_bug.cgi?id=5372 *) +Require Import FunInd. Function odd (n:nat) := match n with | 0 => false diff --git a/test-suite/bugs/closed/5414.v b/test-suite/bugs/closed/5414.v new file mode 100644 index 0000000000..2522a274fb --- /dev/null +++ b/test-suite/bugs/closed/5414.v @@ -0,0 +1,12 @@ +(* Use of idents bound to ltac names in a "match" *) + +Definition foo : Type. +Proof. + let x := fresh "a" in + refine (forall k : nat * nat, let '(x, _) := k in (_ : Type)). + exact (a = a). +Defined. +Goal foo. +intros k. elim k. (* elim because elim keeps names *) +intros. +Check a. (* We check that the name is "a" *) diff --git a/test-suite/bugs/opened/4803.v b/test-suite/bugs/opened/4803.v deleted file mode 100644 index 4541f13d01..0000000000 --- a/test-suite/bugs/opened/4803.v +++ /dev/null @@ -1,48 +0,0 @@ -(* -*- coq-prog-args: ("-compat" "8.4") -*- *) -(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5. If they use*) -Require Import Coq.Lists.List. -Require Import Coq.Vectors.Vector. -Import ListNotations. -Import VectorNotations. -Set Implicit Arguments. -Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T). -Arguments mynil {_}, _. - -Delimit Scope mylist_scope with mylist. -Bind Scope mylist_scope with mylist. -Delimit Scope vector_scope with vector. - -Notation " [ ] " := mynil (format "[ ]") : mylist_scope. -Notation " [ x ] " := (mycons x mynil) : mylist_scope. -Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope. - -(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4. There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *) -Check [ ]%mylist : mylist _. -Check [ ]%list : list _. -Check []%vector : Vector.t _ _. -Check [ _ ]%mylist : mylist _. -Check [ _ ]%list : list _. -Check [ _ ]%vector : Vector.t _ _. -Check [ _ ; _ ]%list : list _. -Check [ _ ; _ ]%vector : Vector.t _ _. -Check [ _ ; _ ]%mylist : mylist _. -Check [ _ ; _ ; _ ]%list : list _. -Check [ _ ; _ ; _ ]%vector : Vector.t _ _. -Check [ _ ; _ ; _ ]%mylist : mylist _. -Check [ _ ; _ ; _ ; _ ]%list : list _. -Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. -Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. - -(** Now check that we can add and then remove notations from the parser *) -(* We should be able to stick some vernacular here to remove [] from the parser *) -Fail Remove Notation "[]". -Goal True. - (* This should not be a syntax error; before moving this file to closed, uncomment this line. *) - (* idtac; []. *) - constructor. -Qed. - -Check { _ : _ & _ }. -Reserved Infix "&" (at level 0). -Fail Remove Infix "&". -(* Check { _ : _ & _ }. *) diff --git a/test-suite/coq-makefile/arg/_CoqProject b/test-suite/coq-makefile/arg/_CoqProject index afdb32e7cf..53dc963997 100644 --- a/test-suite/coq-makefile/arg/_CoqProject +++ b/test-suite/coq-makefile/arg/_CoqProject @@ -1,7 +1,7 @@ -R theories test -R src test -I src --arg "-compat 8.4" +-arg "-w default" src/test_plugin.mlpack src/test.ml4 diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh index d6bb52bb4a..e8291c89da 100755 --- a/test-suite/coq-makefile/coqdoc1/run.sh +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -15,9 +15,7 @@ make install-doc DSTROOT="$PWD/tmp" sort -u > desired <<EOT . ./test -./test/test_plugin.cma ./test/test_plugin.cmi -./test/test_plugin.cmo ./test/test_plugin.cmx ./test/test_plugin.cmxs ./test/test.glob diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh index d6bb52bb4a..e8291c89da 100755 --- a/test-suite/coq-makefile/coqdoc2/run.sh +++ b/test-suite/coq-makefile/coqdoc2/run.sh @@ -15,9 +15,7 @@ make install-doc DSTROOT="$PWD/tmp" sort -u > desired <<EOT . ./test -./test/test_plugin.cma ./test/test_plugin.cmi -./test/test_plugin.cmo ./test/test_plugin.cmx ./test/test_plugin.cmxs ./test/test.glob diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh index f6fb3bcb42..10a200ddee 100755 --- a/test-suite/coq-makefile/mlpack1/run.sh +++ b/test-suite/coq-makefile/mlpack1/run.sh @@ -15,9 +15,7 @@ sort > desired <<EOT . ./test ./test/test.glob -./test/test_plugin.cma ./test/test_plugin.cmi -./test/test_plugin.cmo ./test/test_plugin.cmx ./test/test_plugin.cmxs ./test/test.v diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh index f6fb3bcb42..10a200ddee 100755 --- a/test-suite/coq-makefile/mlpack2/run.sh +++ b/test-suite/coq-makefile/mlpack2/run.sh @@ -15,9 +15,7 @@ sort > desired <<EOT . ./test ./test/test.glob -./test/test_plugin.cma ./test/test_plugin.cmi -./test/test_plugin.cmo ./test/test_plugin.cmx ./test/test_plugin.cmxs ./test/test.v diff --git a/test-suite/coq-makefile/multiroot/run.sh b/test-suite/coq-makefile/multiroot/run.sh index 863c39f500..3cd1ac305f 100755 --- a/test-suite/coq-makefile/multiroot/run.sh +++ b/test-suite/coq-makefile/multiroot/run.sh @@ -19,12 +19,9 @@ sort > desired <<EOT ./test ./test/test.glob ./test/test.cmi -./test/test.cmo ./test/test.cmx ./test/test_aux.cmi -./test/test_aux.cmo ./test/test_aux.cmx -./test/test_plugin.cma ./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.v diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh index f079662631..9f6295d644 100755 --- a/test-suite/coq-makefile/native1/run.sh +++ b/test-suite/coq-makefile/native1/run.sh @@ -18,9 +18,7 @@ sort > desired <<EOT . ./test ./test/test.glob -./test/test_plugin.cma ./test/test_plugin.cmi -./test/test_plugin.cmo ./test/test_plugin.cmx ./test/test_plugin.cmxs ./test/test.v diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh new file mode 100755 index 0000000000..6301aa03c0 --- /dev/null +++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh @@ -0,0 +1,37 @@ +#!/usr/bin/env bash + +set -e + +git clean -dfx + +cat > _CoqProject <<EOT +-I src/ + +./src/test_plugin.mllib +./src/test.ml4 +./src/test.mli +EOT + +mkdir src + +cat > src/test_plugin.mllib <<EOT +Test +EOT + +touch src/test.mli + +cat > src/test.ml4 <<EOT +DECLARE PLUGIN "test" + +let _ = Pre_env.empty_env +EOT + +${COQBIN}coq_makefile -f _CoqProject -o Makefile + +if make VERBOSE=1; then + # make command should have failed (but didn't) + exit 1 +else + # make command should have failed (and it indeed did) + exit 0 +fi diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh new file mode 100755 index 0000000000..991fb4a61d --- /dev/null +++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh @@ -0,0 +1,32 @@ +#!/usr/bin/env bash + +set -e + +git clean -dfx + +cat > _CoqProject <<EOT +-bypass-API +-I src/ + +./src/test_plugin.mllib +./src/test.ml4 +./src/test.mli +EOT + +mkdir src + +cat > src/test_plugin.mllib <<EOT +Test +EOT + +touch src/test.mli + +cat > src/test.ml4 <<EOT +DECLARE PLUGIN "test" + +let _ = Pre_env.empty_env +EOT + +${COQBIN}coq_makefile -f _CoqProject -o Makefile + +make VERBOSE=1 diff --git a/test-suite/coq-makefile/plugin1/run.sh b/test-suite/coq-makefile/plugin1/run.sh index 24ef8c891b..c2d47166fe 100755 --- a/test-suite/coq-makefile/plugin1/run.sh +++ b/test-suite/coq-makefile/plugin1/run.sh @@ -17,12 +17,9 @@ sort > desired <<EOT ./test ./test/test.glob ./test/test.cmi -./test/test.cmo ./test/test.cmx ./test/test_aux.cmi -./test/test_aux.cmo ./test/test_aux.cmx -./test/test_plugin.cma ./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.v diff --git a/test-suite/coq-makefile/plugin2/run.sh b/test-suite/coq-makefile/plugin2/run.sh index 24ef8c891b..c2d47166fe 100755 --- a/test-suite/coq-makefile/plugin2/run.sh +++ b/test-suite/coq-makefile/plugin2/run.sh @@ -17,12 +17,9 @@ sort > desired <<EOT ./test ./test/test.glob ./test/test.cmi -./test/test.cmo ./test/test.cmx ./test/test_aux.cmi -./test/test_aux.cmo ./test/test_aux.cmx -./test/test_plugin.cma ./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.v diff --git a/test-suite/coq-makefile/plugin3/run.sh b/test-suite/coq-makefile/plugin3/run.sh index 24ef8c891b..c2d47166fe 100755 --- a/test-suite/coq-makefile/plugin3/run.sh +++ b/test-suite/coq-makefile/plugin3/run.sh @@ -17,12 +17,9 @@ sort > desired <<EOT ./test ./test/test.glob ./test/test.cmi -./test/test.cmo ./test/test.cmx ./test/test_aux.cmi -./test/test_aux.cmo ./test/test_aux.cmx -./test/test_plugin.cma ./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.v diff --git a/test-suite/coq-makefile/template/src/test.ml4 b/test-suite/coq-makefile/template/src/test.ml4 index 72765abe04..e7d0bfe1f8 100644 --- a/test-suite/coq-makefile/template/src/test.ml4 +++ b/test-suite/coq-makefile/template/src/test.ml4 @@ -1,3 +1,4 @@ +open API open Ltac_plugin DECLARE PLUGIN "test_plugin" let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";; diff --git a/test-suite/coq-makefile/template/src/test_aux.ml b/test-suite/coq-makefile/template/src/test_aux.ml index a01d0865a8..e134abd840 100644 --- a/test-suite/coq-makefile/template/src/test_aux.ml +++ b/test-suite/coq-makefile/template/src/test_aux.ml @@ -1 +1 @@ -let tac = Proofview.tclUNIT () +let tac = API.Proofview.tclUNIT () diff --git a/test-suite/coq-makefile/template/src/test_aux.mli b/test-suite/coq-makefile/template/src/test_aux.mli index 10020f27de..2e7ad1529f 100644 --- a/test-suite/coq-makefile/template/src/test_aux.mli +++ b/test-suite/coq-makefile/template/src/test_aux.mli @@ -1 +1 @@ -val tac : unit Proofview.tactic +val tac : unit API.Proofview.tactic diff --git a/test-suite/failure/int31.v b/test-suite/failure/int31.v index b1d112247f..ed4c9f9c78 100644 --- a/test-suite/failure/int31.v +++ b/test-suite/failure/int31.v @@ -1,4 +1,4 @@ -Require Import Int31 BigN. +Require Import Int31 Cyclic31. Open Scope int31_scope. diff --git a/test-suite/ide/blocking-futures.fake b/test-suite/ide/blocking-futures.fake index b63f09bcfc..541fb798c0 100644 --- a/test-suite/ide/blocking-futures.fake +++ b/test-suite/ide/blocking-futures.fake @@ -4,6 +4,7 @@ # Extraction will force the future computation, assert it is blocking # Example courtesy of Jonathan (jonikelee) # +ADD { Require Coq.extraction.Extraction. } ADD { Require Import List. } ADD { Import ListNotations. } ADD { Definition myrev{A}(l : list A) : {rl : list A | rl = rev l}. } diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index f064dfe763..97fa8e2542 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -80,3 +80,49 @@ fun '(D n m p q) => n + m + p + q : J -> nat The command has indeed failed with message: The constructor D (in type J) expects 3 arguments. +lem1 = +fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl + : forall k : nat * nat, k = k +lem2 = +fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl + : forall k : bool, k = k + +Argument scope is [bool_scope] +lem3 = +fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl + : forall k : nat * nat, k = k +1 subgoal + + x : nat + n, n0 := match x + 0 with + | 0 => 0 + | S _ => 0 + end : nat + e, + e0 := match x + 0 as y return (y = y) with + | 0 => eq_refl + | S n => eq_refl + end : x + 0 = x + 0 + n1, n2 := match x with + | 0 => 0 + | S _ => 0 + end : nat + e1, e2 := match x return (x = x) with + | 0 => eq_refl + | S n => eq_refl + end : x = x + ============================ + x + 0 = 0 +1 subgoal + + p : nat + a, + a0 := match eq_refl as y in (_ = e) return (y = y /\ e = e) with + | eq_refl => conj eq_refl eq_refl + end : eq_refl = eq_refl /\ p = p + a1, + a2 := match eq_refl in (_ = e) return (p = p /\ e = e) with + | eq_refl => conj eq_refl eq_refl + end : p = p /\ p = p + ============================ + eq_refl = eq_refl diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 6a4fd007df..17fee3303d 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -121,3 +121,66 @@ Check fun x => let '(D n m p q) := x in n+m+p+q. (* This used to succeed, being interpreted as "let '{{n, m, p}} := ..." *) Fail Check fun x : J => let '{{n, m, _}} p := x in n + m + p. + +(* Test use of idents bound to ltac names in a "match" *) + +Lemma lem1 : forall k, k=k :>nat * nat. +let x := fresh "aa" in +let y := fresh "bb" in +let z := fresh "cc" in +let k := fresh "dd" in +refine (fun k : nat * nat => match k as x return x = x with (y,z) => eq_refl end). +Qed. +Print lem1. + +Lemma lem2 : forall k, k=k :> bool. +let x := fresh "aa" in +let y := fresh "bb" in +let z := fresh "cc" in +let k := fresh "dd" in +refine (fun k => if k as x return x = x then eq_refl else eq_refl). +Qed. +Print lem2. + +Lemma lem3 : forall k, k=k :>nat * nat. +let x := fresh "aa" in +let y := fresh "bb" in +let z := fresh "cc" in +let k := fresh "dd" in +refine (fun k : nat * nat => let (y,z) as x return x = x := k in eq_refl). +Qed. +Print lem3. + +Lemma lem4 x : x+0=0. +match goal with |- ?y = _ => pose (match y with 0 => 0 | S n => 0 end) end. +match goal with |- ?y = _ => pose (match y as y with 0 => 0 | S n => 0 end) end. +match goal with |- ?y = _ => pose (match y as y return y=y with 0 => eq_refl | S n => eq_refl end) end. +match goal with |- ?y = _ => pose (match y return y=y with 0 => eq_refl | S n => eq_refl end) end. +match goal with |- ?y + _ = _ => pose (match y with 0 => 0 | S n => 0 end) end. +match goal with |- ?y + _ = _ => pose (match y as y with 0 => 0 | S n => 0 end) end. +match goal with |- ?y + _ = _ => pose (match y as y return y=y with 0 => eq_refl | S n => eq_refl end) end. +match goal with |- ?y + _ = _ => pose (match y return y=y with 0 => eq_refl | S n => eq_refl end) end. +Show. + +Lemma lem5 (p:nat) : eq_refl p = eq_refl p. +let y := fresh "n" in (* Checking that y is hidden *) + let z := fresh "e" in (* Checking that z is hidden *) + match goal with + |- ?y = _ => pose (match y as y in _ = z return y=y /\ z=z with eq_refl => conj eq_refl eq_refl end) + end. +let y := fresh "n" in + let z := fresh "e" in + match goal with + |- ?y = _ => pose (match y in _ = z return y=y /\ z=z with eq_refl => conj eq_refl eq_refl end) + end. +let y := fresh "n" in + let z := fresh "e" in + match goal with + |- eq_refl ?y = _ => pose (match eq_refl y in _ = z return y=y /\ z=z with eq_refl => conj eq_refl eq_refl end) + end. +let p := fresh "p" in + let z := fresh "e" in + match goal with + |- eq_refl ?p = _ => pose (match eq_refl p in _ = z return p=p /\ z=z with eq_refl => conj eq_refl eq_refl end) + end. +Show. diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v index 6c514b16ee..1ecd9771eb 100644 --- a/test-suite/output/Extraction_matchs_2413.v +++ b/test-suite/output/Extraction_matchs_2413.v @@ -1,5 +1,7 @@ (** Extraction : tests of optimizations of pattern matching *) +Require Coq.extraction.Extraction. + (** First, a few basic tests *) Definition test1 b := diff --git a/test-suite/output/Int31Syntax.out b/test-suite/output/Int31Syntax.out new file mode 100644 index 0000000000..4e8796c14b --- /dev/null +++ b/test-suite/output/Int31Syntax.out @@ -0,0 +1,14 @@ +I31 + : digits31 int31 +2 + : int31 +660865024 + : int31 +2 + 2 + : int31 +2 + 2 + : int31 + = 4 + : int31 + = 710436486 + : int31 diff --git a/test-suite/output/Int31Syntax.v b/test-suite/output/Int31Syntax.v new file mode 100644 index 0000000000..83be3b976b --- /dev/null +++ b/test-suite/output/Int31Syntax.v @@ -0,0 +1,13 @@ +Require Import Int31 Cyclic31. + +Open Scope int31_scope. +Check I31. (* Would be nice to have I31 : digits->digits->...->int31 + For the moment, I31 : digits31 int31, which is better + than (fix nfun .....) size int31 *) +Check 2. +Check 1000000000000000000. (* = 660865024, after modulo 2^31 *) +Check (add31 2 2). +Check (2+2). +Eval vm_compute in 2+2. +Eval vm_compute in 65675757 * 565675998. +Close Scope int31_scope. diff --git a/test-suite/output/NumbersSyntax.out b/test-suite/output/NumbersSyntax.out deleted file mode 100644 index b2677b6ad1..0000000000 --- a/test-suite/output/NumbersSyntax.out +++ /dev/null @@ -1,67 +0,0 @@ -I31 - : digits31 int31 -2 - : int31 -660865024 - : int31 -2 + 2 - : int31 -2 + 2 - : int31 - = 4 - : int31 - = 710436486 - : int31 -2 - : BigN.t' -1000000000000000000 - : BigN.t' -2 + 2 - : bigN -2 + 2 - : bigN - = 4 - : bigN - = 37151199385380486 - : bigN - = 1267650600228229401496703205376 - : bigN -2 - : BigZ.t_ --1000000000000000000 - : BigZ.t_ -2 + 2 - : BigZ.t_ -2 + 2 - : BigZ.t_ - = 4 - : BigZ.t_ - = 37151199385380486 - : BigZ.t_ - = 1267650600228229401496703205376 - : BigZ.t_ -2 - : BigQ.t_ --1000000000000000000 - : BigQ.t_ -2 + 2 - : bigQ -2 + 2 - : bigQ - = 4 - : bigQ - = 37151199385380486 - : bigQ -6562 # 456 - : BigQ.t_ - = 3281 # 228 - : bigQ - = -1 # 10000 - : bigQ - = 100 - : bigQ - = 515377520732011331036461129765621272702107522001 - # 1267650600228229401496703205376 - : bigQ - = 1 - : bigQ diff --git a/test-suite/output/NumbersSyntax.v b/test-suite/output/NumbersSyntax.v deleted file mode 100644 index 4fbf56ab1d..0000000000 --- a/test-suite/output/NumbersSyntax.v +++ /dev/null @@ -1,50 +0,0 @@ - -Require Import BigQ. - -Open Scope int31_scope. -Check I31. (* Would be nice to have I31 : digits->digits->...->int31 - For the moment, I31 : digits31 int31, which is better - than (fix nfun .....) size int31 *) -Check 2. -Check 1000000000000000000. (* = 660865024, after modulo 2^31 *) -Check (add31 2 2). -Check (2+2). -Eval vm_compute in 2+2. -Eval vm_compute in 65675757 * 565675998. -Close Scope int31_scope. - -Open Scope bigN_scope. -Check 2. -Check 1000000000000000000. -Check (BigN.add 2 2). -Check (2+2). -Eval vm_compute in 2+2. -Eval vm_compute in 65675757 * 565675998. -Eval vm_compute in 2^100. -Close Scope bigN_scope. - -Open Scope bigZ_scope. -Check 2. -Check -1000000000000000000. -Check (BigZ.add 2 2). -Check (2+2). -Eval vm_compute in 2+2. -Eval vm_compute in 65675757 * 565675998. -Eval vm_compute in (-2)^100. -Close Scope bigZ_scope. - -Open Scope bigQ_scope. -Check 2. -Check -1000000000000000000. -Check (BigQ.add 2 2). -Check (2+2). -Eval vm_compute in 2+2. -Eval vm_compute in 65675757 * 565675998. -(* fractions *) -Check (6562 # 456). (* Nota: # is BigQ.Qq i.e. base fractions *) -Eval vm_compute in (BigQ.red (6562 # 456)). -Eval vm_compute in (1/-10000). -Eval vm_compute in (BigQ.red (1/(1/100))). (* back to integers... *) -Eval vm_compute in ((2/3)^(-100)). -Eval vm_compute in BigQ.red ((2/3)^(-1000) * (2/3)^(1000)). -Close Scope bigQ_scope. diff --git a/test-suite/save-logs.sh b/test-suite/save-logs.sh index fb8a1c1b0a..b613621085 100755 --- a/test-suite/save-logs.sh +++ b/test-suite/save-logs.sh @@ -9,7 +9,7 @@ mkdir "$SAVEDIR" # keep this synced with test-suite/Makefile FAILMARK="==========> FAILURE <==========" -FAILED=$(mktemp) +FAILED=$(mktemp /tmp/coq-check-XXXXX) find . '(' -path ./bugs/opened -prune ')' -o '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED" rsync -a --from0 --files-from="$FAILED" . "$SAVEDIR" diff --git a/test-suite/success/Case19.v b/test-suite/success/Case19.v index e59828defe..ce98879a5f 100644 --- a/test-suite/success/Case19.v +++ b/test-suite/success/Case19.v @@ -17,3 +17,22 @@ Fail exists (fun x => with | eq_refl => eq_refl end). +Abort. + +(* Some tests with ltac matching on building "if" and "let" *) + +Goal forall b c d, (if negb b then c else d) = 0. +intros. +match goal with +|- (if ?b then ?c else ?d) = 0 => transitivity (if b then d else c) +end. +Abort. + +Definition swap {A} {B} '((x,y):A*B) := (y,x). + +Goal forall p, (let '(x,y) := swap p in x + y) = 0. +intros. +match goal with +|- (let '(x,y) := ?p in x + y) = 0 => transitivity (let (x,y) := p in x+y) +end. +Abort. diff --git a/test-suite/success/Compat84.v b/test-suite/success/Compat84.v deleted file mode 100644 index 732a024fc1..0000000000 --- a/test-suite/success/Compat84.v +++ /dev/null @@ -1,19 +0,0 @@ -(* -*- coq-prog-args: ("-compat" "8.4") -*- *) - -Goal True. - solve [ constructor 1 ]. Undo. - solve [ econstructor 1 ]. Undo. - solve [ constructor ]. Undo. - solve [ econstructor ]. Undo. - solve [ constructor (fail) ]. Undo. - solve [ econstructor (fail) ]. Undo. - split. -Qed. - -Goal False \/ True. - solve [ constructor (constructor) ]. Undo. - solve [ econstructor (econstructor) ]. Undo. - solve [ constructor 2; constructor ]. Undo. - solve [ econstructor 2; econstructor ]. Undo. - right; esplit. -Qed. diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v index 3bf97c1312..f87f2e2a9d 100644 --- a/test-suite/success/Funind.v +++ b/test-suite/success/Funind.v @@ -1,4 +1,6 @@ +Require Import Coq.funind.FunInd. + Definition iszero (n : nat) : bool := match n with | O => true diff --git a/test-suite/success/InversionSigma.v b/test-suite/success/InversionSigma.v new file mode 100644 index 0000000000..51f33c7ce7 --- /dev/null +++ b/test-suite/success/InversionSigma.v @@ -0,0 +1,40 @@ +Section inversion_sigma. + Local Unset Implicit Arguments. + Context A (B : A -> Prop) (C C' : forall a, B a -> Prop) + (D : forall a b, C a b -> Prop) (E : forall a b c, D a b c -> Prop). + + (* Require that, after destructing sigma types and inverting + equalities, we can subst equalities of variables only, and reduce + down to [eq_refl = eq_refl]. *) + Local Ltac test_inversion_sigma := + intros; + repeat match goal with + | [ H : sig _ |- _ ] => destruct H + | [ H : sigT _ |- _ ] => destruct H + | [ H : sig2 _ _ |- _ ] => destruct H + | [ H : sigT2 _ _ |- _ ] => destruct H + end; simpl in *; + inversion_sigma; + repeat match goal with + | [ H : ?x = ?y |- _ ] => is_var x; is_var y; subst x; simpl in * + end; + match goal with + | [ |- eq_refl = eq_refl ] => reflexivity + end. + + Goal forall (x y : { a : A & { b : { b : B a & C a b } & { d : D a (projT1 b) (projT2 b) & E _ _ _ d } } }) + (p : x = y), p = p. + Proof. test_inversion_sigma. Qed. + + Goal forall (x y : { a : A | { b : { b : B a | C a b } | { d : D a (proj1_sig b) (proj2_sig b) | E _ _ _ d } } }) + (p : x = y), p = p. + Proof. test_inversion_sigma. Qed. + + Goal forall (x y : { a : { a : A & B a } & C _ (projT2 a) & C' _ (projT2 a) }) + (p : x = y), p = p. + Proof. test_inversion_sigma. Qed. + + Goal forall (x y : { a : { a : A & B a } | C _ (projT2 a) & C' _ (projT2 a) }) + (p : x = y), p = p. + Proof. test_inversion_sigma. Qed. +End inversion_sigma. diff --git a/test-suite/success/NumberScopes.v b/test-suite/success/NumberScopes.v index 6d78721075..1558637476 100644 --- a/test-suite/success/NumberScopes.v +++ b/test-suite/success/NumberScopes.v @@ -39,24 +39,3 @@ Definition f_nat (x:nat) := x. Definition f_nat' (x:Nat.t) := x. Check (f_nat 1). Check (f_nat' 1). - -Require Import BigN. -Check (BigN.add 1 2). -Check (BigN.add_comm 1 2). -Check (BigN.min_comm 1 2). -Definition f_bigN (x:bigN) := x. -Check (f_bigN 1). - -Require Import BigZ. -Check (BigZ.add 1 2). -Check (BigZ.add_comm 1 2). -Check (BigZ.min_comm 1 2). -Definition f_bigZ (x:bigZ) := x. -Check (f_bigZ 1). - -Require Import BigQ. -Check (BigQ.add 1 2). -Check (BigQ.add_comm 1 2). -Check (BigQ.min_comm 1 2). -Definition f_bigQ (x:bigQ) := x. -Check (f_bigQ 1).
\ No newline at end of file diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index d8f8042465..8419404925 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -147,6 +147,7 @@ Proof. intros; absurd (p < p); eauto with arith. Qed. +Require Coq.extraction.Extraction. Extraction max. diff --git a/test-suite/success/bigQ.v b/test-suite/success/bigQ.v deleted file mode 100644 index 7fd0cf669d..0000000000 --- a/test-suite/success/bigQ.v +++ /dev/null @@ -1,66 +0,0 @@ -Require Import BigQ. -Import List. - -Definition pi_4_approx_low' := -(5066193963420194617885108698600649932059391557720145469382602092416947640628637390992675949693715109726079394291478795603894419483819297806310615866892414925850691415582239745615128821983865262221858109336884967754871321668348027076234335167119885298878199925731495390387858629042311908406056230882123787019283378509712244687397013657159455607193734144010901984756727174636853404278421831024545476850410085042498464474261035780891759930905778986584183710930670670301831474144997069400304290351567959717683444430666444319233768399342338059169002790777424962570605618705584660815518973602995097110557181643034682308210782171804373210646804613922337450953858508244032293753591878060539465788294318856859293281629951093130167801471787011911886414492513677892193100809508943832528344473873460853362957387889412799458784754514139679847887887544849825173792522272708046699681079289358082661375778523609867456540595586031625044964543428047238934233579184772793670436643502740076366994465457847106782560289782615794595755672643440040123002018908935362541166831619056664637901929131328502017686713274283777724453661234225382109584471950444925886358166551424008707439387934109226545596919797083495958300914344992836193126080289565652575543234385558967555959267746932292860747199382633363026440008828134867747920263181610216905129926037611247017868033961426567047355301676870662406173724238530061264149506666345040372864118731705584795947926329181826992456072045382170981478151356381437136818835196834068650217794381425547036331194595892801393225038235274901050364737353586927051766717037643833477566087835266968086513005761986678747515870298138062157791066648217784877968385924845017637219384732843791052551854695220023477365706464590594542001161575677402761543188277502092362285265847964496740584911576627239093631932307473445797386335961743298553548881544486940399236133577915988716682746485564575640818803540680574730591500432326858763829791848612343662539095316357052823005419355719381626599487868023399182174939253393897549026675976384326749445831606130546375395770778462506203752920470130305293966478109733954117063941901686840180727195741528561335809865193566993349413786715403053579411364371500063193205131503024022217701373077790337150298315820556080596579100618643147698304927957576213733526923182742441048553793831725592624850721293495085399785588171300815789795594858916409701139277050529011775828846362873246196866089783324522718656445008090114701320562608474099248873638488023114015981013142490827777895317580810590743940417298263300561876701828404744082864248409230009391001735746615476377303707782123483770118391136826609366946585715225248587168403619476143657107412319421501162805102723455593551478028055839072686207007765300258935153546418515706362733656094770289090398825190320430416955807878686642673124733998295439657633866090085982598765253268688814792672416195730086607425842181518560588819896560847103627615434844684536463752986969865794019299978956052589825441828842338163389851892617560591840546654410705167593310272272965900821031821380595084783691324416454359888103920904935692840264474003367023256964191100139001239923263691779167792867186165635514824889759796850863175082506408142175595463676408992027105356481220754473245821534527625758942093801142305560662681150069082553674495761075895588095760081401141419460482860852822686860785424514171214889677926763812031823537071721974799922995763666175738785000806081164280471363125324839717808977470218218571800106898347366938927189989988149888641129263448064762730769285877330997355234347773807099829665997515649429224335217107760728789764718885665291038706425454675746218345291274054088843647602239258308472486102933167465443294268551209015027897159307743987020521392788721231001835675584104894174434637260464035122611721657641428625505184886116917149318963070896162119215386541876236027342810162765609201440423207771441367926085768438143507025739041041240810056881304230519058117534418374553879198061289605354335880794397478047346975609179199801003098836622253165101961484972165230151495472006888128587168049198312469715081555662345452800468933420359802645393289853553618279788400476187713990872203669487294118461245455333004125835663010526985716431187034663870796866708678078952110615910196519835267441831874676895301527286826106517027821074816850326548617513767142627360001181210946100011774672126943957522004190414960909074050454565964857276407084991922274068961845339154089866785707764290964299529444616711194034827611771558783466230353209661849406004241580029437779784290315347968833708422223285859451369907260780956405036020581705441364379616715041818815829810906212826084485200785283123265202151252852134381195424724503189247411069117189489985791487434549080447866370484866697404176437230771558469231403088139693477706784802801265075586678597768511791952562627345622499328 - # 100788726492580594349650258277496659410917619472657560321971265983799894639441017438166498752997098978003489632843381325240982516059309714013145358125224597827602157516585886911710102182473475545864474089191789296685473601331678556438310133356793199956062857423397512495293688453655805536015029176541424005214818033707522950635262669828538132795615008381824067071229426026518897202246241637377064076189277685257166926338187911595052586669184297526234794666364657344206795357967279911782849686515024121916258300642000317525374433525235296287037535618423661645124459323811792936193272341688261801253469089129439519903538495370298752436267926761998785090092411372633429302950606054074205533246665546979112178855223925266166034953000200646676762301817000435641690517142795144469005596172113586738287118865058604922865654348297975054956781513943444060257230946224520058527667925776273088622386666860662470481606622952298649177217986593047495967209669116410592230626047083795555559776477430548946990993890380787911273437967786556742804566652408275798339221179283430482118140020742719695900657696142739101628984271513292954605191778803974738871043737934546460016184719168074062912083778327025499841998124431899131874519812228674255796948879306477894924710085384116453080236862135706628989104070747737689294987000148388110561753028594988959655591699155508380909698460304884908709246116411180876105681720036833487450945730831039969246996849503525429840196651386469599438064049723005123629385485140945945416764414133189625489032807860400751723995946290581976152580477047961138617997133510128194027510895265424780627975864980749945631413855375897945293107842908479797077570371447220506451229526132919408351287454305932886749170523056147842439813407002950370505941417426433452282518739345666494683448699945734453214481915512562995906034771246088038719298959180199052759295868161570318718927430655393250250811804905393113074074574608255523847592006804881016594060188745212933427473833239777228852952217878690668413947367586040297784502192683200664398064682201012931468052982448022330449955215606614483165425935154496289535573901139223034819824408001205784146243892228030383941863746839845526558421740316887532141893650230936137269356278754487130882868595412163277284772124736531380334814212708066069618080153747333573454834500999083737284449542481264971030785043701582134343596645346132964567391370300568578875509971483039720438955919863275044932311289587494336123538202079503922025306586828117649623642521324286648529829664567232756108169459356549144779085080036654897525078792273443307070502103724611233768453196294899770515940520895908289018412144327894912660060761908970811602375085884115384049610753387776858733798341463052471017393165656926510611173543365663267563198760597092606598728110197523695339144204179424646442294307593146446562536865057987897899655645968129515654148044008249646703504419478535298270862753806142083172190778193001810574370442181909146645889199829207284871551220439225371051511970054965951914399901815408791418836185742573331879114400013259342896515702942707292473805188905427717363630137869116872433627556880809120353079342030725196065815470427569172350436988386579444534375353968759750750178342190349607711313840613843718547859929387259163285524671855725511880656411741012446023392964655239624520090988149679656514996202498334816938716757663800773997302639681907686195671083505910700098597156238624351157219093280177066146218516478636356056420098245995113668018177690728654922707281126889313941750547830163078886329630807850633273613622550216189245162735650139455042125252043274668279981753287687674520319519360593091620297805736177366738063651905396783336064579717230286821545930579779462534206093794040878198825916141099864730374109311705285661056855668930671948265232862757146615431791375559792290479316263924560826544387396762768331402198937951439504767950821089741987629257538953417586416459087855138539304027013800937360598578194413362672871055543854633921502486683911956250444582746421552178164852341035733290405311280719066037175324627429434912416361334254696649419037348733709488576582107382055914938194078813926926742828297826939120316120573453588052056773875836843924877773978390546387248009519202370375478981843515393806263037580338009594022254079586380520797699651840576286033587273591899639699077044271208886940540056794360292760863657703246410020854088849880453524038877935317875884698324859548991680533307680053872403383516589028793015681082435908524045497475001609824047204954932626536311826911363867426654549346914317405110707189532251727848751560224936842128628673253616256326013555922159336370177663785738170802777550686079119049748734352584409583136667752555307842739679930698964098088960000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%bigQ -. - -Definition pi_4_approx_high' := -(5066193963420194617885108698600649932059391557720145469382602092416947640628637390992675949693715109726079394291478795603894419483819297806310615866892414925850691415582239745615128821983865262221858109336884967754871321668348027076234335167119885298878199925731495390387858629042311908406056230882123787019283378509712244687397013657159455607193734144010901984756727174636853404278421831024545476850410085042498464474261035780891759930905778986584183710930670670301831474144997069400304290351567959717683444430666444319233768399342338059169002790777424962570605618705584660815518973602995097110557181643034682308210788409308322071457087096445676662503017187903223859814905546579050729173916234740628466315449085686468204847296426235788544874405450791749423436215032927889914519102361378633666267941326393265376660400091389373564825046526561381561278586121772300141564909333667988204680492088607706214346458601842899721615765319505314310192693665547163360402786722105590252780194994950097926184146718893770363322073641336811404180286358079915338791029818581497746089864894356686643882883410392601500048021013346713450539807687779704798018559373507951388092945938366448668853081682176581336156031434604604833692503597621519809826880683536141897075567053733515342478008373282599947520770191238802249392773327261328133194484586433840861730959791563023761306622956165536481335792721379318928171897265310054788931201902441066997927781894934061720760080768154565282051604447333036111267534150649674590201404453202347064545359869105856798745664471694795576801148562495225166002814304124970965817043547048503388910163287916513427409193998045119986267987892522931703487420953769290650229176116308194977201080691718825944370436642709192983358059711255925052564016519597530235976618244111239816418652282585432539731271068892992142956810775762851238126881225206289553948196520384709574383566733478326330112084307565420647201107231840508040019131253750047046446929758911912155202166566751947087545292626353331520202690130850009389387290465497377022080531269511355734944672010542204118978272180881335465227900174033380001851066811103401787656367819132934758616060307366679580043123632565656840669377840733018248707250548277181001911990237151790533341326223932843775840498222236867608395855700891719880219904948672458645420169533565809609056209006342663841718949396996175294237942265325043426430990062217643279654512512640557763489491751115437780462208361129433667449740743123546232162409802316714286708788831227582498585478334315076725145986771341647015244092760289407649044493584479944044779273447198382196766547779885914425854375158084417582279211000449529495605127376707776277159376010648950025135061284601443461110447113346277147728593420397807946636800365109579479211273476195727270004743568492888900356505584731622538401071221591141889158461271000051210318027818802379539544396973228585821742794928813630781709195703717312953337431290682263448669168179857644544116657440168099166467471736180072984407514757289757495435699300593165669101965987430482600019222913485092771346963058673132443387835726110205958057187517487684058179749952286341120230051432903482992282688283815697442898155194928723360957436110770317998431272108100149791425689283090777721270428030993332057319821685391144252815655146410678839177846108260765981523812232294638190350688210999605869296307711846463311346627138400477211801219366400312514793356564308532012682051019030257269068628100171220662165246389309014292764479226570049772046255291379151017129899157296574099437276707879597755725339406865738613810979022640265737120949077721294633786520294559343155148383011293584240192753971366644780434237846862975993387453786681995831719537733846579480995517357440575781962659282856696638992709756358478461648462532279323701121386551383509193782388241965285971965887701816406255233933761008649762854363984142178331798953040874526844255758512982810004271235810681505829473926495256537353108899526434200682024946218302499640511518360332022463196599199779172637638655415918976955930735312156870786600023896830267884391447789311101069654521354446521135407720085038662159974712373018912537116964809382149581004863115431780452188813210275393919111435118030412595133958954313836191108258769640843644195537185904547405641078708492098917460393911427237155683288565433183738513871595286090814836422982384810033331519971102974091067660369548406192526284519976668985518575216481570167748402860759832933071281814538397923687510782620605409323050353840034866296214149657376249634795555007199540807313397329050410326609108411299737760271566308288500400587417017113933243099961248847368789383209110747378488312550109911605079801570534271874115018095746872468910162721975463388518648962869080447866370484866697404176437230771558469231403088139693477706784802801265075586678597768511791952562627345622499328 - # 100788726492580594349650258277496659410917619472657560321971265983799894639441017438166498752997098978003489632843381325240982516059309714013145358125224597827602157516585886911710102182473475545864474089191789296685473601331678556438310133356793199956062857423397512495293688453655805536015029176541424005214818033707522950635262669828538132795615008381824067071229426026518897202246241637377064076189277685257166926338187911595052586669184297526234794666364657344206795357967279911782849686515024121916258300642000317525374433525235296287037535618423661645124459323811792936193272341688261801253469089129439519903538495370298752436267926761998785090092411372633429302950606054074205533246665546979112178855223925266166034953000200646676762301817000435641690517142795144469005596172113586738287118865058604922865654348297975054956781513943444060257230946224520058527667925776273088622386666860662470481606622952298649177217986593047495967209669116410592230626047083795555559776477430548946990993890380787911273437967786556742804566652408275798339221179283430482118140020742719695900657696142739101628984271513292954605191778803974738871043737934546460016184719168074062912083778327025499841998124431899131874519812228674255796948879306477894924710085384116453080236862135706628989104070747737689294987000148388110561753028594988959655591699155508380909698460304884908709246116411180876105681720036833487450945730831039969246996849503525429840196651386469599438064049723005123629385485140945945416764414133189625489032807860400751723995946290581976152580477047961138617997133510128194027510895265424780627975864980749945631413855375897945293107842908479797077570371447220506451229526132919408351287454305932886749170523056147842439813407002950370505941417426433452282518739345666494683448699945734453214481915512562995906034771246088038719298959180199052759295868161570318718927430655393250250811804905393113074074574608255523847592006804881016594060188745212933427473833239777228852952217878690668413947367586040297784502192683200664398064682201012931468052982448022330449955215606614483165425935154496289535573901139223034819824408001205784146243892228030383941863746839845526558421740316887532141893650230936137269356278754487130882868595412163277284772124736531380334814212708066069618080153747333573454834500999083737284449542481264971030785043701582134343596645346132964567391370300568578875509971483039720438955919863275044932311289587494336123538202079503922025306586828117649623642521324286648529829664567232756108169459356549144779085080036654897525078792273443307070502103724611233768453196294899770515940520895908289018412144327894912660060761908970811602375085884115384049610753387776858733798341463052471017393165656926510611173543365663267563198760597092606598728110197523695339144204179424646442294307593146446562536865057987897899655645968129515654148044008249646703504419478535298270862753806142083172190778193001810574370442181909146645889199829207284871551220439225371051511970054965951914399901815408791418836185742573331879114400013259342896515702942707292473805188905427717363630137869116872433627556880809120353079342030725196065815470427569172350436988386579444534375353968759750750178342190349607711313840613843718547859929387259163285524671855725511880656411741012446023392964655239624520090988149679656514996202498334816938716757663800773997302639681907686195671083505910700098597156238624351157219093280177066146218516478636356056420098245995113668018177690728654922707281126889313941750547830163078886329630807850633273613622550216189245162735650139455042125252043274668279981753287687674520319519360593091620297805736177366738063651905396783336064579717230286821545930579779462534206093794040878198825916141099864730374109311705285661056855668930671948265232862757146615431791375559792290479316263924560826544387396762768331402198937951439504767950821089741987629257538953417586416459087855138539304027013800937360598578194413362672871055543854633921502486683911956250444582746421552178164852341035733290405311280719066037175324627429434912416361334254696649419037348733709488576582107382055914938194078813926926742828297826939120316120573453588052056773875836843924877773978390546387248009519202370375478981843515393806263037580338009594022254079586380520797699651840576286033587273591899639699077044271208886940540056794360292760863657703246410020854088849880453524038877935317875884698324859548991680533307680053872403383516589028793015681082435908524045497475001609824047204954932626536311826911363867426654549346914317405110707189532251727848751560224936842128628673253616256326013555922159336370177663785738170802777550686079119049748734352584409583136667752555307842739679930698964098088960000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%bigQ -. - -Fixpoint numden_Rcontfrac_tailrecB (accu: list bigZ) (n1 d1: bigZ) (n2 d2: bigZ) (fuel: nat) {struct fuel}: - (list bigZ * bigQ * bigQ) := - let default := (rev_append accu nil, BigQ.div (BigQ.Qz n1) (BigQ.Qz d1), BigQ.div (BigQ.Qz n2) (BigQ.Qz d2)) in - match fuel with - | O => default - | S fuel' => - let '(q1, r1) := BigZ.div_eucl n1 d1 in - let '(q2, r2) := BigZ.div_eucl n2 d2 in - match BigZ.eqb q1 q2 with - | false => default - | true => - let r1_is_zero := BigZ.eqb r1 0 in - let r2_is_zero := BigZ.eqb r2 0 in - match Bool.eqb r1_is_zero r2_is_zero with - | false => default - | true => - match r1_is_zero with - | true => - match BigZ.eqb q1 1 with - | true => (rev_append accu nil, 1%bigQ, 1%bigQ) - | false => (rev_append ((q1 - 1)%bigZ :: accu) nil, 1%bigQ, 1%bigQ) - end - | false => numden_Rcontfrac_tailrecB (q1 :: accu) d1 r1 d2 r2 fuel' - end - end - end - end. - -Definition Bnum b := - match b with - | BigQ.Qz t => t - | BigQ.Qq n d => - if (d =? BigN.zero)%bigN then 0%bigZ else n - end. - -Definition Bden b := - match b with - | BigQ.Qz _ => 1%bigN - | BigQ.Qq _ d => if (d =? BigN.zero)%bigN then 1%bigN else d - end. - -Definition rat_Rcontfrac_tailrecB q1 q2 := - numden_Rcontfrac_tailrecB nil (Bnum q1) (BigZ.Pos (Bden q1)) (Bnum q2) (BigZ.Pos (Bden q2)). - -Definition pi_4_contfrac := - rat_Rcontfrac_tailrecB pi_4_approx_low' pi_4_approx_high' 3000. - -(* The following used to fail because of a non canonical representation of 0 in -the bytecode interpreter. Bug reported privately by Tahina Ramananandro. *) -Goal pi_4_contfrac = pi_4_contfrac. -vm_compute. -reflexivity. -Qed. diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index 0086e090bd..89be144152 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +Require Coq.extraction.Extraction. Require Import Arith. Require Import List. diff --git a/test-suite/success/extraction_dep.v b/test-suite/success/extraction_dep.v index 11bb25fda0..e770cf779a 100644 --- a/test-suite/success/extraction_dep.v +++ b/test-suite/success/extraction_dep.v @@ -1,6 +1,8 @@ (** Examples of code elimination inside modules during extraction *) +Require Coq.extraction.Extraction. + (** NB: we should someday check the produced code instead of simply running the commands. *) diff --git a/test-suite/success/extraction_impl.v b/test-suite/success/extraction_impl.v index dfdeff82ff..5bf807b1c6 100644 --- a/test-suite/success/extraction_impl.v +++ b/test-suite/success/extraction_impl.v @@ -4,6 +4,8 @@ (** NB: we should someday check the produced code instead of simply running the commands. *) +Require Coq.extraction.Extraction. + (** Bug #4243, part 1 *) Inductive dnat : nat -> Type := diff --git a/test-suite/success/extraction_polyprop.v b/test-suite/success/extraction_polyprop.v index 7215bd9905..936d838c50 100644 --- a/test-suite/success/extraction_polyprop.v +++ b/test-suite/success/extraction_polyprop.v @@ -3,6 +3,8 @@ code that segfaults. See Table.error_singleton_become_prop or S. Glondu's thesis for more details. *) +Require Coq.extraction.Extraction. + Definition f {X} (p : (nat -> X) * True) : X * nat := (fst p 0, 0). diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 2fa7704941..789854b2d6 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -181,6 +181,8 @@ Record wrap (A : Type) := { unwrap : A; unwrap2 : A }. Definition term (x : wrap nat) := x.(unwrap). Definition term' (x : wrap nat) := let f := (@unwrap2 nat) in f x. + +Require Coq.extraction.Extraction. Recursive Extraction term term'. (*Unset Printing Primitive Projection Parameters.*) |