diff options
Diffstat (limited to 'test-suite')
85 files changed, 1305 insertions, 411 deletions
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/3612.v b/test-suite/bugs/closed/3612.v index 73709268a4..33e5d532ad 100644 --- a/test-suite/bugs/closed/3612.v +++ b/test-suite/bugs/closed/3612.v @@ -39,7 +39,6 @@ Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P) p = q. Declare ML Module "ltac_plugin". -Declare ML Module "coretactics". Set Default Proof Mode "Classic". diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v index 179f81e668..a664a1ef1d 100644 --- a/test-suite/bugs/closed/3649.v +++ b/test-suite/bugs/closed/3649.v @@ -3,7 +3,6 @@ (* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0 coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *) Declare ML Module "ltac_plugin". -Declare ML Module "coretactics". Set Default Proof Mode "Classic". Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). Reserved Notation "x = y" (at level 70, no associativity). @@ -14,7 +13,6 @@ Axiom admit : forall {T}, T. Notation "A -> B" := (forall (_ : A), B) : type_scope. Reserved Infix "o" (at level 40, left associativity). Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. -Ltac constr_eq a b := let test := constr:(@idpath _ _ : a = b) in idtac. Global Set Primitive Projections. Delimit Scope morphism_scope with morphism. Record PreCategory := 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/3943.v b/test-suite/bugs/closed/3943.v new file mode 100644 index 0000000000..5e5ba816f9 --- /dev/null +++ b/test-suite/bugs/closed/3943.v @@ -0,0 +1,50 @@ +(* File reduced by coq-bug-finder from original input, then from 9492 lines to 119 lines *) +(* coqc version 8.5beta1 (January 2015) compiled on Jan 18 2015 7:27:36 with OCaml 3.12.1 + coqtop version 8.5beta1 (January 2015) *) + +Set Typeclasses Dependency Order. + +Inductive paths {A : Type} (a : A) : A -> Type := + idpath : paths a a. +Arguments idpath {A a} , [A] a. +Notation "x = y" := (@paths _ x y) : type_scope. +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with idpath => idpath end. + +Set Implicit Arguments. +Delimit Scope morphism_scope with morphism. +Delimit Scope category_scope with category. +Delimit Scope object_scope with object. + +Record PreCategory := Build_PreCategory' { + object :> Type; + morphism : object -> object -> Type; + identity : forall x, morphism x x; + compose : forall s d d', + morphism d d' + -> morphism s d + -> morphism s d' }. +Arguments identity {!C%category} / x%object : rename. +Arguments compose {!C%category} / {s d d'}%object (m1 m2)%morphism : rename. + +Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) := { + morphism_inverse : morphism C d s; + left_inverse : compose morphism_inverse m = identity _; + right_inverse : compose m morphism_inverse = identity _ }. +Arguments morphism_inverse {C s d} m {_}. +Local Notation "m ^-1" := (morphism_inverse m) (at level 3, format "m '^-1'") : morphism_scope. + +Class Isomorphic {C : PreCategory} s d := { + morphism_isomorphic :> morphism C s d; + isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic }. +Coercion morphism_isomorphic : Isomorphic >-> morphism. + +Variable C : PreCategory. +Variables s d : C. + +Definition path_isomorphic (i j : Isomorphic s d) +: @morphism_isomorphic _ _ _ i = @morphism_isomorphic _ _ _ j -> i = j. +Admitted. + +Definition ap_morphism_inverse_path_isomorphic (i j : Isomorphic s d) p q +: ap (fun e : Isomorphic s d => e^-1)%morphism (path_isomorphic i j p) = q.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4250.v b/test-suite/bugs/closed/4250.v new file mode 100644 index 0000000000..74cacf559a --- /dev/null +++ b/test-suite/bugs/closed/4250.v @@ -0,0 +1,11 @@ +Require Import FunInd. +Require Vector. +Generalizable All Variables. + +Definition f `{n:nat , u:Vector.t A n} := n. + +Function f2 {A:Type} {n:nat} {v:Vector.t A n} : nat := n. + +(* fails with "The reference A was not found in the current environment." *) +Function f3 `{n:nat , u:Vector.t A n} := u. +Check R_f3_complete.
\ No newline at end of file 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/5205.v b/test-suite/bugs/closed/5205.v new file mode 100644 index 0000000000..406f37a4b1 --- /dev/null +++ b/test-suite/bugs/closed/5205.v @@ -0,0 +1,6 @@ +Definition foo (n : nat) (m : nat) : nat := m. + +Arguments foo {_} _, _ _. + +Check foo 1 1. +Check foo (n:=1) 1. diff --git a/test-suite/bugs/closed/5365.v b/test-suite/bugs/closed/5365.v new file mode 100644 index 0000000000..be360d24d2 --- /dev/null +++ b/test-suite/bugs/closed/5365.v @@ -0,0 +1,13 @@ + +Inductive TupleT : nat -> Type := +| nilT : TupleT 0 +| consT {n} A : (A -> TupleT n) -> TupleT (S n). + +Inductive Tuple : forall n, TupleT n -> Type := + nil : Tuple _ nilT +| cons {n A} (x : A) (F : A -> TupleT n) : Tuple _ (F x) -> Tuple _ (consT A F). + +Inductive TupleMap : forall n, TupleT n -> TupleT n -> Type := + tmNil : TupleMap _ nilT nilT +| tmCons {n} {A B : Type} (F : A -> TupleT n) (G : B -> TupleT n) + : (forall x, sigT (fun y => TupleMap _ (F x) (G y))) -> TupleMap _ (consT A F) (consT B G). 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/closed/5618.v b/test-suite/bugs/closed/5618.v new file mode 100644 index 0000000000..ab88a88f44 --- /dev/null +++ b/test-suite/bugs/closed/5618.v @@ -0,0 +1,9 @@ +Require Import FunInd. + +Function test {T} (v : T) (x : nat) : nat := + match x with + | 0 => 0 + | S x' => test v x' + end. + +Check R_test_complete.
\ No newline at end of file diff --git a/test-suite/bugs/closed/5641.v b/test-suite/bugs/closed/5641.v new file mode 100644 index 0000000000..9f3246f33d --- /dev/null +++ b/test-suite/bugs/closed/5641.v @@ -0,0 +1,6 @@ +Set Universe Polymorphism. + +Definition foo@{i j} (A : Type@{i}) : Type@{j}. +Proof. +abstract (exact ltac:(abstract (exact A))). +Defined. diff --git a/test-suite/bugs/closed/HoTT_coq_123.v b/test-suite/bugs/closed/HoTT_coq_123.v index cd9cad4064..7bed956f3e 100644 --- a/test-suite/bugs/closed/HoTT_coq_123.v +++ b/test-suite/bugs/closed/HoTT_coq_123.v @@ -104,11 +104,15 @@ Record Functor (C D : PreCategory) := morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d) }. +(** Workaround to simpl losing universe constraints, see bug #5645. *) +Ltac simpl' := + simpl; match goal with [ |- ?P ] => let T := type of P in idtac end. + Global Instance trunc_forall `{Funext} `{P : A -> Type} `{forall a, IsTrunc n (P a)} : IsTrunc n (forall a, P a) | 100. Proof. generalize dependent P. - induction n as [ | n' IH]; (simpl; intros P ?). + induction n as [ | n' IH]; (simpl'; intros P ?). - admit. - pose (fun f g => trunc_equiv (@apD10 A P f g) ^-1); admit. Defined. 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/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/Tauto.v b/test-suite/failure/Tauto.v index d91d159d9c..19976b41bd 100644 --- a/test-suite/failure/Tauto.v +++ b/test-suite/failure/Tauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/clash_cons.v b/test-suite/failure/clash_cons.v index b3fbff680b..1761cc437d 100644 --- a/test-suite/failure/clash_cons.v +++ b/test-suite/failure/clash_cons.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/fixpoint1.v b/test-suite/failure/fixpoint1.v index c2b521c214..0739982442 100644 --- a/test-suite/failure/fixpoint1.v +++ b/test-suite/failure/fixpoint1.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v index 8db2785837..312dc48bea 100644 --- a/test-suite/failure/guard.v +++ b/test-suite/failure/guard.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/illtype1.v b/test-suite/failure/illtype1.v index 8ed3af1ce4..fdd1bddd88 100644 --- a/test-suite/failure/illtype1.v +++ b/test-suite/failure/illtype1.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) 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/failure/positivity.v b/test-suite/failure/positivity.v index 8089de2bf0..b21204b9e4 100644 --- a/test-suite/failure/positivity.v +++ b/test-suite/failure/positivity.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/redef.v b/test-suite/failure/redef.v index c8dc6303f7..c49dbd7cae 100644 --- a/test-suite/failure/redef.v +++ b/test-suite/failure/redef.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/search.v b/test-suite/failure/search.v index 648ab0820c..fae6cd6f3b 100644 --- a/test-suite/failure/search.v +++ b/test-suite/failure/search.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) 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/ideal-features/Apply.v b/test-suite/ideal-features/Apply.v index c8e9af216e..85680e94b9 100644 --- a/test-suite/ideal-features/Apply.v +++ b/test-suite/ideal-features/Apply.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/misc/deps-checksum.sh b/test-suite/misc/deps-checksum.sh index 1e2afb7540..e07612b84c 100755 --- a/test-suite/misc/deps-checksum.sh +++ b/test-suite/misc/deps-checksum.sh @@ -1,4 +1,4 @@ -rm -f misc/deps/*/*.vo +rm -f misc/deps/A/*.vo misc/deps/B/*.vo $coqc -R misc/deps/A A misc/deps/A/A.v $coqc -R misc/deps/B A misc/deps/B/A.v $coqc -R misc/deps/B A misc/deps/B/B.v diff --git a/test-suite/misc/deps-order.sh b/test-suite/misc/deps-order.sh index 375b706f0a..00c5eb1bd5 100755 --- a/test-suite/misc/deps-order.sh +++ b/test-suite/misc/deps-order.sh @@ -1,7 +1,7 @@ # Check that both coqdep and coqtop/coqc supports -R # Check that both coqdep and coqtop/coqc takes the later -R # See bugs 2242, 2337, 2339 -rm -f misc/deps/*/*.vo +rm -f misc/deps/lib/*.vo misc/deps/client/*.vo tmpoutput=`mktemp /tmp/coqcheck.XXXXXX` $coqdep -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 | head -n 1 > $tmpoutput diff -u misc/deps/deps.out $tmpoutput 2>&1 diff --git a/test-suite/misc/printers.sh b/test-suite/misc/printers.sh index c822d0eb37..28e7dc362f 100755 --- a/test-suite/misc/printers.sh +++ b/test-suite/misc/printers.sh @@ -1,3 +1,3 @@ -printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | grep Unbound +printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | egrep "Error|Unbound" if [ $? = 0 ]; then exit 1; else exit 0; fi diff --git a/test-suite/modules/polymorphism.v b/test-suite/modules/polymorphism.v new file mode 100644 index 0000000000..63eaa382dc --- /dev/null +++ b/test-suite/modules/polymorphism.v @@ -0,0 +1,81 @@ +Set Universe Polymorphism. + +(** Tests for module subtyping of polymorphic terms *) + +Module Type S. + +Section Foo. + +Universes i j. +Constraint i <= j. + +Parameter foo : Type@{i} -> Type@{j}. + +End Foo. + +End S. + +(** Same constraints *) + +Module OK_1. + +Definition foo@{i j} (A : Type@{i}) : Type@{j} := A. + +End OK_1. + +Module OK_1_Test : S := OK_1. + +(** More general constraints *) + +Module OK_2. + +Inductive X@{i} : Type@{i} :=. +Definition foo@{i j} (A : Type@{i}) : Type@{j} := X@{j}. + +End OK_2. + +Module OK_2_Test : S := OK_2. + +(** Wrong instance length *) + +Module KO_1. + +Definition foo@{i} (A : Type@{i}) : Type@{i} := A. + +End KO_1. + +Fail Module KO_Test_1 : S := KO_1. + +(** Less general constraints *) + +Module KO_2. + +Section Foo. + +Universe i j. +Constraint i < j. + +Definition foo (A : Type@{i}) : Type@{j} := A. + +End Foo. + +End KO_2. + +Fail Module KO_Test_2 : S := KO_2. + +(** Less general constraints *) + +Module KO_3. + +Section Foo. + +Universe i j. +Constraint i = j. + +Definition foo (A : Type@{i}) : Type@{j} := A. + +End Foo. + +End KO_3. + +Fail Module KO_Test_3 : S := KO_3. diff --git a/test-suite/modules/polymorphism2.v b/test-suite/modules/polymorphism2.v new file mode 100644 index 0000000000..7e3327eee0 --- /dev/null +++ b/test-suite/modules/polymorphism2.v @@ -0,0 +1,87 @@ +Set Universe Polymorphism. + +(** Tests for module subtyping of polymorphic terms *) + +Module Type S. + +Section Foo. + +Universes i j. +Constraint i <= j. + +Inductive foo : Type@{i} -> Type@{j} :=. + +End Foo. + +End S. + +(** Same constraints *) + +Module OK_1. + +Section Foo. + +Universes i j. +Constraint i <= j. + +Inductive foo : Type@{i} -> Type@{j} :=. + +End Foo. + +End OK_1. + +Module OK_1_Test : S := OK_1. + +(** More general constraints *) + +Module OK_2. + +Inductive foo@{i j} : Type@{i} -> Type@{j} :=. + +End OK_2. + +Module OK_2_Test : S := OK_2. + +(** Wrong instance length *) + +Module KO_1. + +Inductive foo@{i} : Type@{i} -> Type@{i} :=. + +End KO_1. + +Fail Module KO_Test_1 : S := KO_1. + +(** Less general constraints *) + +Module KO_2. + +Section Foo. + +Universe i j. +Constraint i < j. + +Inductive foo : Type@{i} -> Type@{j} :=. + +End Foo. + +End KO_2. + +Fail Module KO_Test_2 : S := KO_2. + +(** Less general constraints *) + +Module KO_3. + +Section Foo. + +Universe i j. +Constraint i = j. + +Inductive foo : Type@{i} -> Type@{j} :=. + +End Foo. + +End KO_3. + +Fail Module KO_Test_3 : S := KO_3. 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/Notations.v b/test-suite/output/Notations.v index 2ccca829d6..b9985a594f 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -1,3 +1,14 @@ +(* Bug 5568, don't warn for notations in repeated module import *) + +Module foo. +Notation compose := (fun g f => g f). +Notation "g & f" := (compose g f) (at level 10). +End foo. + +Import foo. +Import foo. +Import foo. + (**********************************************************************) (* Notations for if and let (submitted by Roland Zumkeller) *) 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/output/RecognizePluginWarning.out b/test-suite/output/RecognizePluginWarning.out new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/test-suite/output/RecognizePluginWarning.out diff --git a/test-suite/output/RecognizePluginWarning.v b/test-suite/output/RecognizePluginWarning.v new file mode 100644 index 0000000000..cd667bbd00 --- /dev/null +++ b/test-suite/output/RecognizePluginWarning.v @@ -0,0 +1,5 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "extraction-logical-axiom") -*- *) + +(* Test that mentioning a warning defined in plugins works. The failure +mode here is that these result in a warning about unknown warnings, since the +plugins are not known at command line parsing time. *) diff --git a/test-suite/output/UsePluginWarning.out b/test-suite/output/UsePluginWarning.out new file mode 100644 index 0000000000..47409f3ec5 --- /dev/null +++ b/test-suite/output/UsePluginWarning.out @@ -0,0 +1 @@ +type foo = __ diff --git a/test-suite/output/UsePluginWarning.v b/test-suite/output/UsePluginWarning.v new file mode 100644 index 0000000000..c6e0054641 --- /dev/null +++ b/test-suite/output/UsePluginWarning.v @@ -0,0 +1,7 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-extraction-logical-axiom") -*- *) + +Require Extraction. +Axiom foo : Prop. + +Extraction foo. + diff --git a/test-suite/output/Warnings.out b/test-suite/output/Warnings.out new file mode 100644 index 0000000000..a70f8ca45a --- /dev/null +++ b/test-suite/output/Warnings.out @@ -0,0 +1,3 @@ +File "stdin", line 4, characters 0-22: +Warning: Projection value has no head constant: fun x : B => x in canonical +instance a of b, ignoring it. [projection-no-head-constant,typechecker] diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v new file mode 100644 index 0000000000..7465442cab --- /dev/null +++ b/test-suite/output/Warnings.v @@ -0,0 +1,5 @@ +(* Term in warning was not printed in the right environment at some time *) +Record A := { B:Type; b:B->B }. +Definition a B := {| B:=B; b:=fun x => x |}. +Canonical Structure a. + 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/Check.v b/test-suite/success/Check.v index e4ee351c3a..0f677a8495 100644 --- a/test-suite/success/Check.v +++ b/test-suite/success/Check.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) 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/Field.v b/test-suite/success/Field.v index 438e461357..018b22c489 100644 --- a/test-suite/success/Field.v +++ b/test-suite/success/Field.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) 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/FunindExtraction_compat86.v b/test-suite/success/FunindExtraction_compat86.v new file mode 100644 index 0000000000..8912197d2f --- /dev/null +++ b/test-suite/success/FunindExtraction_compat86.v @@ -0,0 +1,506 @@ +(* -*- coq-prog-args: ("-compat" "8.6") -*- *) + +Definition iszero (n : nat) : bool := + match n with + | O => true + | _ => false + end. + +Functional Scheme iszero_ind := Induction for iszero Sort Prop. + +Lemma toto : forall n : nat, n = 0 -> iszero n = true. +intros x eg. + functional induction iszero x; simpl. +trivial. +inversion eg. +Qed. + + +Function ftest (n m : nat) : nat := + match n with + | O => match m with + | O => 0 + | _ => 1 + end + | S p => 0 + end. +(* MS: FIXME: apparently can't define R_ftest_complete. Rest of the file goes through. *) + +Lemma test1 : forall n m : nat, ftest n m <= 2. +intros n m. + functional induction ftest n m; auto. +Qed. + +Lemma test2 : forall m n, ~ 2 = ftest n m. +Proof. +intros n m;intro H. +functional inversion H ftest. +Qed. + +Lemma test3 : forall n m, ftest n m = 0 -> (n = 0 /\ m = 0) \/ n <> 0. +Proof. +functional inversion 1 ftest;auto. +Qed. + + +Require Import Arith. +Lemma test11 : forall m : nat, ftest 0 m <= 2. +intros m. + functional induction ftest 0 m. +auto. +auto. +auto with *. +Qed. + +Function lamfix (m n : nat) {struct n } : nat := + match n with + | O => m + | S p => lamfix m p + end. + +(* Parameter v1 v2 : nat. *) + +Lemma lamfix_lem : forall v1 v2 : nat, lamfix v1 v2 = v1. +intros v1 v2. + functional induction lamfix v1 v2. +trivial. +assumption. +Defined. + + + +(* polymorphic function *) +Require Import List. + +Functional Scheme app_ind := Induction for app Sort Prop. + +Lemma appnil : forall (A : Set) (l l' : list A), l' = nil -> l = l ++ l'. +intros A l l'. + functional induction app A l l'; intuition. + rewrite <- H0; trivial. +Qed. + + + + + +Require Export Arith. + + +Function trivfun (n : nat) : nat := + match n with + | O => 0 + | S m => trivfun m + end. + + +(* essaie de parametre variables non locaux:*) + +Parameter varessai : nat. + +Lemma first_try : trivfun varessai = 0. + functional induction trivfun varessai. +trivial. +assumption. +Defined. + + + Functional Scheme triv_ind := Induction for trivfun Sort Prop. + +Lemma bisrepetita : forall n' : nat, trivfun n' = 0. +intros n'. + functional induction trivfun n'. +trivial. +assumption. +Qed. + + + + + + + +Function iseven (n : nat) : bool := + match n with + | O => true + | S (S m) => iseven m + | _ => false + end. + + +Function funex (n : nat) : nat := + match iseven n with + | true => n + | false => match n with + | O => 0 + | S r => funex r + end + end. + + +Function nat_equal_bool (n m : nat) {struct n} : bool := + match n with + | O => match m with + | O => true + | _ => false + end + | S p => match m with + | O => false + | S q => nat_equal_bool p q + end + end. + + +Require Export Div2. +Require Import Nat. +Functional Scheme div2_ind := Induction for div2 Sort Prop. +Lemma div2_inf : forall n : nat, div2 n <= n. +intros n. + functional induction div2 n. +auto. +auto. + +apply le_S. +apply le_n_S. +exact IHn0. +Qed. + +(* reuse this lemma as a scheme:*) + +Function nested_lam (n : nat) : nat -> nat := + match n with + | O => fun m : nat => 0 + | S n' => fun m : nat => m + nested_lam n' m + end. + + +Lemma nest : forall n m : nat, nested_lam n m = n * m. +intros n m. + functional induction nested_lam n m; simpl;auto. +Qed. + + +Function essai (x : nat) (p : nat * nat) {struct x} : nat := + let (n, m) := (p: nat*nat) in + match n with + | O => 0 + | S q => match x with + | O => 1 + | S r => S (essai r (q, m)) + end + end. + +Lemma essai_essai : + forall (x : nat) (p : nat * nat), let (n, m) := p in 0 < n -> 0 < essai x p. +intros x p. + functional induction essai x p; intros. +inversion H. +auto with arith. + auto with arith. +Qed. + +Function plus_x_not_five'' (n m : nat) {struct n} : nat := + let x := nat_equal_bool m 5 in + let y := 0 in + match n with + | O => y + | S q => + let recapp := plus_x_not_five'' q m in + match x with + | true => S recapp + | false => S recapp + end + end. + +Lemma notplusfive'' : forall x y : nat, y = 5 -> plus_x_not_five'' x y = x. +intros a b. + functional induction plus_x_not_five'' a b; intros hyp; simpl; auto. +Qed. + +Lemma iseq_eq : forall n m : nat, n = m -> nat_equal_bool n m = true. +intros n m. + functional induction nat_equal_bool n m; simpl; intros hyp; auto. +rewrite <- hyp in y; simpl in y;tauto. +inversion hyp. +Qed. + +Lemma iseq_eq' : forall n m : nat, nat_equal_bool n m = true -> n = m. +intros n m. + functional induction nat_equal_bool n m; simpl; intros eg; auto. +inversion eg. +inversion eg. +Qed. + + +Inductive istrue : bool -> Prop := + istrue0 : istrue true. + +Functional Scheme add_ind := Induction for add Sort Prop. + +Lemma inf_x_plusxy' : forall x y : nat, x <= x + y. +intros n m. + functional induction add n m; intros. +auto with arith. +auto with arith. +Qed. + + +Lemma inf_x_plusxy'' : forall x : nat, x <= x + 0. +intros n. +unfold plus. + functional induction plus n 0; intros. +auto with arith. +apply le_n_S. +assumption. +Qed. + +Lemma inf_x_plusxy''' : forall x : nat, x <= 0 + x. +intros n. + functional induction plus 0 n; intros; auto with arith. +Qed. + +Function mod2 (n : nat) : nat := + match n with + | O => 0 + | S (S m) => S (mod2 m) + | _ => 0 + end. + +Lemma princ_mod2 : forall n : nat, mod2 n <= n. +intros n. + functional induction mod2 n; simpl; auto with arith. +Qed. + +Function isfour (n : nat) : bool := + match n with + | S (S (S (S O))) => true + | _ => false + end. + +Function isononeorfour (n : nat) : bool := + match n with + | S O => true + | S (S (S (S O))) => true + | _ => false + end. + +Lemma toto'' : forall n : nat, istrue (isfour n) -> istrue (isononeorfour n). +intros n. + functional induction isononeorfour n; intros istr; simpl; + inversion istr. +apply istrue0. +destruct n. inversion istr. +destruct n. tauto. +destruct n. inversion istr. +destruct n. inversion istr. +destruct n. tauto. +simpl in *. inversion H0. +Qed. + +Lemma toto' : forall n m : nat, n = 4 -> istrue (isononeorfour n). +intros n. + functional induction isononeorfour n; intros m istr; inversion istr. +apply istrue0. +rewrite H in y; simpl in y;tauto. +Qed. + +Function ftest4 (n m : nat) : nat := + match n with + | O => match m with + | O => 0 + | S q => 1 + end + | S p => match m with + | O => 0 + | S r => 1 + end + end. + +Lemma test4 : forall n m : nat, ftest n m <= 2. +intros n m. + functional induction ftest n m; auto with arith. +Qed. + +Lemma test4' : forall n m : nat, ftest4 (S n) m <= 2. +intros n m. +assert ({n0 | n0 = S n}). +exists (S n);reflexivity. +destruct H as [n0 H1]. +rewrite <- H1;revert H1. + functional induction ftest4 n0 m. +inversion 1. +inversion 1. + +auto with arith. +auto with arith. +Qed. + +Function ftest44 (x : nat * nat) (n m : nat) : nat := + let (p, q) := (x: nat*nat) in + match n with + | O => match m with + | O => 0 + | S q => 1 + end + | S p => match m with + | O => 0 + | S r => 1 + end + end. + +Lemma test44 : + forall (pq : nat * nat) (n m o r s : nat), ftest44 pq n (S m) <= 2. +intros pq n m o r s. + functional induction ftest44 pq n (S m). +auto with arith. +auto with arith. +auto with arith. +auto with arith. +Qed. + +Function ftest2 (n m : nat) {struct n} : nat := + match n with + | O => match m with + | O => 0 + | S q => 0 + end + | S p => ftest2 p m + end. + +Lemma test2' : forall n m : nat, ftest2 n m <= 2. +intros n m. + functional induction ftest2 n m; simpl; intros; auto. +Qed. + +Function ftest3 (n m : nat) {struct n} : nat := + match n with + | O => 0 + | S p => match m with + | O => ftest3 p 0 + | S r => 0 + end + end. + +Lemma test3' : forall n m : nat, ftest3 n m <= 2. +intros n m. + functional induction ftest3 n m. +intros. +auto. +intros. +auto. +intros. +simpl. +auto. +Qed. + +Function ftest5 (n m : nat) {struct n} : nat := + match n with + | O => 0 + | S p => match m with + | O => ftest5 p 0 + | S r => ftest5 p r + end + end. + +Lemma test5 : forall n m : nat, ftest5 n m <= 2. +intros n m. + functional induction ftest5 n m. +intros. +auto. +intros. +auto. +intros. +simpl. +auto. +Qed. + +Function ftest7 (n : nat) : nat := + match ftest5 n 0 with + | O => 0 + | S r => 0 + end. + +Lemma essai7 : + forall (Hrec : forall n : nat, ftest5 n 0 = 0 -> ftest7 n <= 2) + (Hrec0 : forall n r : nat, ftest5 n 0 = S r -> ftest7 n <= 2) + (n : nat), ftest7 n <= 2. +intros hyp1 hyp2 n. + functional induction ftest7 n; auto. +Qed. + +Function ftest6 (n m : nat) {struct n} : nat := + match n with + | O => 0 + | S p => match ftest5 p 0 with + | O => ftest6 p 0 + | S r => ftest6 p r + end + end. + + +Lemma princ6 : + (forall n m : nat, n = 0 -> ftest6 0 m <= 2) -> + (forall n m p : nat, + ftest6 p 0 <= 2 -> ftest5 p 0 = 0 -> n = S p -> ftest6 (S p) m <= 2) -> + (forall n m p r : nat, + ftest6 p r <= 2 -> ftest5 p 0 = S r -> n = S p -> ftest6 (S p) m <= 2) -> + forall x y : nat, ftest6 x y <= 2. +intros hyp1 hyp2 hyp3 n m. +generalize hyp1 hyp2 hyp3. +clear hyp1 hyp2 hyp3. + functional induction ftest6 n m; auto. +Qed. + +Lemma essai6 : forall n m : nat, ftest6 n m <= 2. +intros n m. + functional induction ftest6 n m; simpl; auto. +Qed. + +(* Some tests with modules *) +Module M. +Function test_m (n:nat) : nat := + match n with + | 0 => 0 + | S n => S (S (test_m n)) + end. + +Lemma test_m_is_double : forall n, div2 (test_m n) = n. +Proof. +intros n. +functional induction (test_m n). +reflexivity. +simpl;rewrite IHn0;reflexivity. +Qed. +End M. +(* We redefine a new Function with the same name *) +Function test_m (n:nat) : nat := + pred n. + +Lemma test_m_is_pred : forall n, test_m n = pred n. +Proof. +intro n. +functional induction (test_m n). (* the test_m_ind to use is the last defined saying that test_m = pred*) +reflexivity. +Qed. + +(* Checks if the dot notation are correctly treated in infos *) +Lemma M_test_m_is_double : forall n, div2 (M.test_m n) = n. +intro n. +(* here we should apply M.test_m_ind *) +functional induction (M.test_m n). +reflexivity. +simpl;rewrite IHn0;reflexivity. +Qed. + +Import M. +(* Now test_m is the one which defines double *) + +Lemma test_m_is_double : forall n, div2 (M.test_m n) = n. +intro n. +(* here we should apply M.test_m_ind *) +functional induction (test_m n). +reflexivity. +simpl;rewrite IHn0;reflexivity. +Qed. + +Extraction iszero. 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/ROmega3.v b/test-suite/success/ROmega3.v new file mode 100644 index 0000000000..fd4ff260b5 --- /dev/null +++ b/test-suite/success/ROmega3.v @@ -0,0 +1,31 @@ + +Require Import ZArith ROmega. +Local Open Scope Z_scope. + +(** Benchmark provided by Chantal Keller, that romega used to + solve far too slowly (compared to omega or lia). *) + +Parameter v4 : Z. +Parameter v3 : Z. +Parameter o4 : Z. +Parameter s5 : Z. +Parameter v2 : Z. +Parameter o5 : Z. +Parameter s6 : Z. +Parameter v1 : Z. +Parameter o6 : Z. +Parameter s7 : Z. +Parameter v0 : Z. +Parameter o7 : Z. + +Lemma lemma_5833 : + ~ 16 * v4 + (8 * v3 + (-8192 * o4 + (-4096 * s5 + (4 * v2 + + (-4096 * o5 + (-2048 * s6 + (2 * v1 + (-2048 * o6 + + (-1024 * s7 + (v0 + -1024 * o7)))))))))) >= 8192 +\/ + 16 * v4 + (8 * v3 + (-8192 * o4 + (-4096 * s5 + (4 * v2 + + (-4096 * o5 + (-2048 * s6 + (2 * v1 + (-2048 * o6 + + (-1024 * s7 + (v0 + -1024 * o7)))))))))) >= 1024. +Proof. +Timeout 1 romega. (* should take a few milliseconds, not seconds *) +Timeout 1 Qed. (* ditto *) 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/Tauto.v b/test-suite/success/Tauto.v index 767f15be72..bffd96044d 100644 --- a/test-suite/success/Tauto.v +++ b/test-suite/success/Tauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v index 023cb5f59d..87296744c4 100644 --- a/test-suite/success/TestRefine.v +++ b/test-suite/success/TestRefine.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/abstract_poly.v b/test-suite/success/abstract_poly.v new file mode 100644 index 0000000000..b736b734fd --- /dev/null +++ b/test-suite/success/abstract_poly.v @@ -0,0 +1,20 @@ +Set Universe Polymorphism. + +Inductive path@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := refl : path x x. +Inductive unit@{i} : Type@{i} := tt. + +Lemma foo@{i j} : forall (m n : unit@{i}) (P : unit -> Type@{j}), path m n -> P m -> P n. +Proof. +intros m n P e p. +abstract (rewrite e in p; exact p). +Defined. + +Check foo_subproof@{Set Set}. + +Lemma bar : forall (m n : unit) (P : unit -> Type), path m n -> P m -> P n. +Proof. +intros m n P e p. +abstract (rewrite e in p; exact p). +Defined. + +Check bar_subproof@{Set Set Set}. 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/eauto.v b/test-suite/success/eauto.v index 160f2d9deb..9b0ff1c8fe 100644 --- a/test-suite/success/eauto.v +++ b/test-suite/success/eauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v index 724e2998ef..055434df01 100644 --- a/test-suite/success/eqdecide.v +++ b/test-suite/success/eqdecide.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index 0086e090bd..4a509da89e 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -1,11 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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/inds_type_sec.v b/test-suite/success/inds_type_sec.v index c729b23ce7..7e9095dfd7 100644 --- a/test-suite/success/inds_type_sec.v +++ b/test-suite/success/inds_type_sec.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 1ed731f50f..35d7929877 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v index 45c1a5e584..c4c5623897 100644 --- a/test-suite/success/mutual_ind.v +++ b/test-suite/success/mutual_ind.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) 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.*) diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index d595cbc2b8..ce1c33fc40 100644 --- a/test-suite/success/unfold.v +++ b/test-suite/success/unfold.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/typeclasses/NewSetoid.v b/test-suite/typeclasses/NewSetoid.v index 49f20a23f5..37d197a15c 100644 --- a/test-suite/typeclasses/NewSetoid.v +++ b/test-suite/typeclasses/NewSetoid.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |