diff options
Diffstat (limited to 'test-suite')
58 files changed, 538 insertions, 411 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/3330.v b/test-suite/bugs/closed/3330.v index e3b5e94356..672fb3f131 100644 --- a/test-suite/bugs/closed/3330.v +++ b/test-suite/bugs/closed/3330.v @@ -41,6 +41,8 @@ Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function Open Scope function_scope. +Set Printing Universes. Set Printing All. + Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. @@ -156,7 +158,8 @@ Delimit Scope morphism_scope with morphism. Delimit Scope category_scope with category. Delimit Scope object_scope with object. - +Set Printing Universes. +Set Printing All. Record PreCategory := Build_PreCategory' { object :> Type; @@ -1069,7 +1072,7 @@ Section Adjunction. Variable F : Functor C D. Variable G : Functor D C. - Let Adjunction_Type := + Let Adjunction_Type := Eval simpl in (hom_functor D) o (F^op, 1) <~=~> (hom_functor C) o (1, G). Record AdjunctionHom := 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/4366.v b/test-suite/bugs/closed/4366.v index 6a5e9a4023..403c2d2026 100644 --- a/test-suite/bugs/closed/4366.v +++ b/test-suite/bugs/closed/4366.v @@ -10,6 +10,6 @@ end. Goal True. Proof. pose (v := stupid 24). -Timeout 2 vm_compute in v. +Timeout 4 vm_compute in v. exact I. Qed. 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/closed/5578.v b/test-suite/bugs/closed/5578.v new file mode 100644 index 0000000000..5bcdaa2f18 --- /dev/null +++ b/test-suite/bugs/closed/5578.v @@ -0,0 +1,57 @@ +(* File reduced by coq-bug-finder from original input, then from 1549 lines to 298 lines, then from 277 lines to 133 lines, then from 985 lines to 138 lines, then from 206 lines to 139 lines, then from 203 lines to 142 lines, then from 262 lines to 152 lines, then from 567 lines to 151 lines, then from 3746 lines to 151 lines, then from 577 lines to 151 lines, then from 187 lines to 151 lines, thenfrom 981 lines to 940 lines, then from 938 lines to 175 lines, then from 589 lines to 205 lines, then from 3797 lines to 205 lines, then from 628 lines to 206 lines, then from 238 lines to 205 lines, then from 1346 lines to 213 lines, then from 633 lines to 214 lines, then from 243 lines to 213 lines, then from 5656 lines to 245 lines, then from 661 lines to 272 lines, then from 3856 lines to 352 lines, then from 1266 lines to 407 lines, then from 421 lines to 406 lines, then from 424 lines to 91 lines, then from 105 lines to 91 lines, then from 85 lines to 55 lines, then from 69 lines to 55 lines *) +(* coqc version trunk (May 2017) compiled on May 30 2017 13:28:59 with OCaml +4.02.3 + coqtop version jgross-Leopard-WS:/home/jgross/Downloads/coq/coq-trunk,trunk (fd36c0451c26e44b1b7e93299d3367ad2d35fee3) *) + +Class Proper {A} (R : A -> A -> Prop) (m : A) := mkp : R m m. +Definition respectful {A B} (R : A -> A -> Prop) (R' : B -> B -> Prop) (f g : A -> B) := forall x y, R x y -> R' (f x) (g y). +Set Implicit Arguments. + +Class EqDec (A : Set) := { + eqb : A -> A -> bool ; + eqb_leibniz : forall x y, eqb x y = true <-> x = y +}. + +Infix "?=" := eqb (at level 70) : eq_scope. + +Inductive Comp : Set -> Type := +| Bind : forall (A B : Set), Comp B -> (B -> Comp A) -> Comp A. + +Open Scope eq_scope. + +Goal forall (Rat : Set) (PositiveMap_t : Set -> Set) + type (t : type) (interp_type_list_message interp_type_rand interp_type_message : nat -> Set), + (forall eta : nat, PositiveMap_t (interp_type_rand eta) -> interp_type_list_message eta -> interp_type_message eta) -> + ((nat -> Rat) -> Prop) -> + forall (interp_type_sbool : nat -> Set) (interp_type0 : type -> nat -> Set), + (forall eta : nat, + (interp_type_list_message eta -> interp_type_message eta) -> PositiveMap_t (interp_type_rand eta) -> interp_type0 t eta) + -> (forall (t0 : type) (eta : nat), EqDec (interp_type0 t0 eta)) + -> (bool -> Comp bool) -> False. + clear. + intros Rat PositiveMap_t type t interp_type_list_message interp_type_rand interp_type_message adv negligible interp_type_sbool + interp_type interp_term_fixed_t_x + EqDec_interp_type ret_bool. + assert (forall f adv' k + (lem : forall (eta : nat) (evil_rands rands : PositiveMap_t +(interp_type_rand eta)), + (interp_term_fixed_t_x eta (adv eta evil_rands) rands + ?= interp_term_fixed_t_x eta (adv eta evil_rands) rands) = true), + (forall (eta : nat), Proper (respectful eq eq) (f eta)) + -> negligible + (fun eta : nat => + f eta ( + (Bind (k eta) (fun rands => + ret_bool (interp_term_fixed_t_x eta (adv' eta) rands ?= interp_term_fixed_t_x eta (adv' eta) rands)))))). + Undo. + assert (forall f adv' k + (lem : forall (eta : nat) (rands : PositiveMap_t +(interp_type_rand eta)), + (interp_term_fixed_t_x eta (adv' eta) rands ?= interp_term_fixed_t_x eta (adv' eta) rands) = true), + (forall (eta : nat), Proper (respectful eq eq) (f eta)) + -> negligible + (fun eta : nat => + f eta ( + (Bind (k eta) (fun rands => + ret_bool (interp_term_fixed_t_x eta (adv' eta) rands ?= interp_term_fixed_t_x eta (adv' eta) rands)))))). + (* Error: Anomaly "Signature and its instance do not match." Please report at http://coq.inria.fr/bugs/. *)
\ No newline at end of file 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/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v new file mode 100644 index 0000000000..a978f6b901 --- /dev/null +++ b/test-suite/coqchk/cumulativity.v @@ -0,0 +1,67 @@ +Set Universe Polymorphism. +Set Inductive Cumulativity. +Set Printing Universes. + +Inductive List (A: Type) := nil | cons : A -> List A -> List A. + +Section ListLift. + Universe i j. + + Constraint i < j. + + Definition LiftL {A} : List@{i} A -> List@{j} A := fun x => x. + +End ListLift. + +Lemma LiftL_Lem A (l : List A) : l = LiftL l. +Proof. reflexivity. Qed. + +Section ListLower. + Universe i j. + + Constraint i < j. + + Definition LowerL {A : Type@{i}} : List@{j} A -> List@{i} A := fun x => x. + +End ListLower. + +Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l. +Proof. reflexivity. Qed. +(* +I disable these tests because cqochk can't process them when compiled with + ocaml-4.02.3+32bit and camlp5-4.16 which is the case for Travis! + + I have added this file (including the commented parts below) in + test-suite/success/cumulativity.v which doesn't run coqchk on them. +*) +(* Inductive Tp := tp : Type -> Tp. *) + +(* Section TpLift. *) +(* Universe i j. *) + +(* Constraint i < j. *) + +(* Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x. *) + +(* End TpLift. *) + +(* Lemma LiftC_Lem (t : Tp) : LiftTp t = t. *) +(* Proof. reflexivity. Qed. *) + +(* Section TpLower. *) +(* Universe i j. *) + +(* Constraint i < j. *) + +(* Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x. *) + +(* End TpLower. *) + + +(* Section subtyping_test. *) +(* Universe i j. *) +(* Constraint i < j. *) + +(* Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2. *) + +(* End subtyping_test. *)
\ No newline at end of file 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/cumulativity.v b/test-suite/success/cumulativity.v new file mode 100644 index 0000000000..ebf817cfc5 --- /dev/null +++ b/test-suite/success/cumulativity.v @@ -0,0 +1,65 @@ +Set Universe Polymorphism. +Set Inductive Cumulativity. +Set Printing Universes. + +Inductive List (A: Type) := nil | cons : A -> List A -> List A. + +Section ListLift. + Universe i j. + + Constraint i < j. + + Definition LiftL {A} : List@{i} A -> List@{j} A := fun x => x. + +End ListLift. + +Lemma LiftL_Lem A (l : List A) : l = LiftL l. +Proof. reflexivity. Qed. + +Section ListLower. + Universe i j. + + Constraint i < j. + + Definition LowerL {A : Type@{i}} : List@{j} A -> List@{i} A := fun x => x. + +End ListLower. + +Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l. +Proof. reflexivity. Qed. + +Inductive Tp := tp : Type -> Tp. + +Section TpLift. + Universe i j. + + Constraint i < j. + + Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x. + +End TpLift. + +Lemma LiftC_Lem (t : Tp) : LiftTp t = t. +Proof. reflexivity. Qed. + +Section TpLower. + Universe i j. + + Constraint i < j. + + Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x. + +End TpLower. + + +Section subtyping_test. + Universe i j. + Constraint i < j. + + Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2. + +End subtyping_test. + +Record A : Type := { a :> Type; }. + +Record B (X : A) : Type := { b : X; }.
\ No newline at end of file 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/polymorphism.v b/test-suite/success/polymorphism.v index 66ff55edcb..ecc988507c 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -352,3 +352,35 @@ Module Anonymous. Check collapsethemiddle@{_ _}. End Anonymous. + +Module F. + Context {A B : Type}. + Definition foo : Type := B. +End F. + +Set Universe Polymorphism. + +Cumulative Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }. + +Section test_letin_subtyping. + Universe i j k i' j' k'. + Constraint j < j'. + + Context (W : Type) (X : box@{i j k} W). + Definition Y := X : box@{i' j' k'} W. + + Universe i1 j1 k1 i2 j2 k2. + Constraint i1 < i2. + Constraint k2 < k1. + Context (V : Type). + + Definition Z : box@{i1 j1 k1} V := {| unwrap := V |}. + Definition Z' : box@{i2 j2 k2} V := {| unwrap := V |}. + Lemma ZZ' : @eq (box@{i2 j2 k2} V) Z Z'. + Proof. + Set Printing All. Set Printing Universes. + cbv. + reflexivity. + Qed. + +End test_letin_subtyping. 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.*) |