diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2016-01-26 16:56:33 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-01-26 16:56:33 +0100 |
| commit | 164c6861860e6b52818c031f901ffeff91fca16a (patch) | |
| tree | 4f91d20c890c25915e7b28226c663b94a8cfb0d3 /test-suite | |
| parent | 91dbeab8eef959c3f64960909ca69d4e68c8198d (diff) | |
Imported Upstream version 8.5upstream/8.5
Diffstat (limited to 'test-suite')
98 files changed, 1485 insertions, 123 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 31b21290..207f25ed 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -154,6 +154,9 @@ summary.log: $(SHOW) SUMMARY $(HIDE)$(MAKE) --quiet summary > "$@" +report: summary.log + $(HIDE)if grep -F 'Error!' summary.log ; then false; fi + ####################################################################### # Regression (and progression) tests ####################################################################### @@ -349,7 +352,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v fi; \ } > "$@" -# Additionnal dependencies for module tests +# Additional dependencies for module tests $(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik.vo modules/%.vo: modules/%.v $(HIDE)$(coqtop) -R modules Mods -compile $< diff --git a/test-suite/bench/lists-100.v b/test-suite/bench/lists-100.v index 352c7cea..5c64716c 100644 --- a/test-suite/bench/lists-100.v +++ b/test-suite/bench/lists-100.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/bench/lists_100.v b/test-suite/bench/lists_100.v index 352c7cea..5c64716c 100644 --- a/test-suite/bench/lists_100.v +++ b/test-suite/bench/lists_100.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/bugs/closed/3249.v b/test-suite/bugs/closed/3249.v index d41d2317..71d457b0 100644 --- a/test-suite/bugs/closed/3249.v +++ b/test-suite/bugs/closed/3249.v @@ -5,7 +5,7 @@ Ltac ret_and_left T := lazymatch eval hnf in t with | ?a /\ ?b => constr:(proj1 T) | forall x : ?T', @?f x => - constr:(fun x : T' => $(let fx := constr:(T x) in + constr:(fun x : T' => ltac:(let fx := constr:(T x) in let t := ret_and_left fx in - exact t)$) + exact t)) end. diff --git a/test-suite/bugs/closed/3257.v b/test-suite/bugs/closed/3257.v new file mode 100644 index 00000000..d8aa6a04 --- /dev/null +++ b/test-suite/bugs/closed/3257.v @@ -0,0 +1,5 @@ +Require Import Setoid Morphisms Basics. +Lemma foo A B (P : B -> Prop) : + pointwise_relation _ impl (fun z => A -> P z) P. +Proof. + Fail reflexivity. diff --git a/test-suite/bugs/closed/3285.v b/test-suite/bugs/closed/3285.v index 25162329..68e6b738 100644 --- a/test-suite/bugs/closed/3285.v +++ b/test-suite/bugs/closed/3285.v @@ -1,7 +1,7 @@ Goal True. Proof. match goal with - | _ => let x := constr:($(fail)$) in idtac + | _ => let x := constr:(ltac:(fail)) in idtac | _ => idtac end. Abort. diff --git a/test-suite/bugs/closed/3286.v b/test-suite/bugs/closed/3286.v index b08b7ab3..701480fc 100644 --- a/test-suite/bugs/closed/3286.v +++ b/test-suite/bugs/closed/3286.v @@ -6,20 +6,20 @@ Ltac make_apply_under_binders_in lem H := | forall x : ?T, @?P x => let ret := constr:(fun x' : T => let Hx := H x' in - $(let ret' := tac lem Hx in - exact ret')$) in + ltac:(let ret' := tac lem Hx in + exact ret')) in match eval cbv zeta in ret with | fun x => Some (@?P x) => let P' := (eval cbv zeta in P) in constr:(Some P') end - | _ => let ret := constr:($(match goal with + | _ => let ret := constr:(ltac:(match goal with | _ => (let H' := fresh in pose H as H'; apply lem in H'; exact (Some H')) | _ => exact (@None nat) end - )$) in + )) in let ret' := (eval cbv beta zeta in ret) in constr:(ret') | _ => constr:(@None nat) diff --git a/test-suite/bugs/closed/3314.v b/test-suite/bugs/closed/3314.v index fb3791af..a5782298 100644 --- a/test-suite/bugs/closed/3314.v +++ b/test-suite/bugs/closed/3314.v @@ -1,9 +1,9 @@ Require Import TestSuite.admit. Set Universe Polymorphism. Definition Lift -: $(let U1 := constr:(Type) in +: ltac:(let U1 := constr:(Type) in let U0 := constr:(Type : U1) in - exact (U0 -> U1))$ + exact (U0 -> U1)) := fun T => T. Fail Check nat:Prop. (* The command has indeed failed with message: diff --git a/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v index e6a50449..e3b5e943 100644 --- a/test-suite/bugs/closed/3330.v +++ b/test-suite/bugs/closed/3330.v @@ -8,7 +8,7 @@ Inductive foo : Type@{l} := bar : foo . Section MakeEq. Variables (a : foo@{i}) (b : foo@{j}). - Let t := $(let ty := type of b in exact ty)$. + Let t := ltac:(let ty := type of b in exact ty). Definition make_eq (x:=b) := a : t. End MakeEq. diff --git a/test-suite/bugs/closed/3347.v b/test-suite/bugs/closed/3347.v index 63d5c7a5..dcf5394e 100644 --- a/test-suite/bugs/closed/3347.v +++ b/test-suite/bugs/closed/3347.v @@ -1,7 +1,7 @@ Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 12653 lines to 12453 lines, then from 11673 lines to 681 lines, then from 693 lines to 469 lines, then from 375 lines to 56 lines *) Set Universe Polymorphism. -Notation Type1 := $(let U := constr:(Type) in let gt := constr:(Set : U) in exact U)$ (only parsing). +Notation Type1 := ltac:(let U := constr:(Type) in let gt := constr:(Set : U) in exact U) (only parsing). Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. Inductive Unit : Type1 := tt : Unit. Fail Check Unit : Set. (* [Check Unit : Set] should fail if [Type1] is defined correctly *) diff --git a/test-suite/bugs/closed/3354.v b/test-suite/bugs/closed/3354.v index 14b66db3..a635285f 100644 --- a/test-suite/bugs/closed/3354.v +++ b/test-suite/bugs/closed/3354.v @@ -1,5 +1,5 @@ Set Universe Polymorphism. -Notation Type1 := $(let U := constr:(Type) in let gt := constr:(Set : U) in exact U)$ (only parsing). +Notation Type1 := ltac:(let U := constr:(Type) in let gt := constr:(Set : U) in exact U) (only parsing). Inductive Empty : Type1 := . Fail Check Empty : Set. (* Toplevel input, characters 15-116: diff --git a/test-suite/bugs/closed/3467.v b/test-suite/bugs/closed/3467.v index 7e371162..88ae0305 100644 --- a/test-suite/bugs/closed/3467.v +++ b/test-suite/bugs/closed/3467.v @@ -1,5 +1,5 @@ Module foo. - Notation x := $(exact I)$. + Notation x := ltac:(exact I). End foo. Module bar. Include foo. diff --git a/test-suite/bugs/closed/3487.v b/test-suite/bugs/closed/3487.v index 03c60a8b..1321a859 100644 --- a/test-suite/bugs/closed/3487.v +++ b/test-suite/bugs/closed/3487.v @@ -1,4 +1,4 @@ -Notation bar := $(exact I)$. +Notation bar := ltac:(exact I). Notation foo := bar (only parsing). Class baz := { x : False }. Instance: baz. diff --git a/test-suite/bugs/closed/3554.v b/test-suite/bugs/closed/3554.v new file mode 100644 index 00000000..13a79cc8 --- /dev/null +++ b/test-suite/bugs/closed/3554.v @@ -0,0 +1 @@ +Example foo (f : forall {_ : Type}, Type) : Type. diff --git a/test-suite/bugs/closed/3682.v b/test-suite/bugs/closed/3682.v index 2a282d22..9d37d1a2 100644 --- a/test-suite/bugs/closed/3682.v +++ b/test-suite/bugs/closed/3682.v @@ -3,4 +3,4 @@ Class Foo. Definition bar `{Foo} (x : Set) := Set. Instance: Foo. Definition bar1 := bar nat. -Definition bar2 := bar $(admit)$. +Definition bar2 := bar ltac:(admit). diff --git a/test-suite/bugs/closed/3684.v b/test-suite/bugs/closed/3684.v index f7b13738..130d5777 100644 --- a/test-suite/bugs/closed/3684.v +++ b/test-suite/bugs/closed/3684.v @@ -1,5 +1,5 @@ Require Import TestSuite.admit. Definition foo : Set. Proof. - refine ($(abstract admit)$). + refine (ltac:(abstract admit)). Qed. diff --git a/test-suite/bugs/closed/3685.v b/test-suite/bugs/closed/3685.v index a5bea34a..7a0c3e6f 100644 --- a/test-suite/bugs/closed/3685.v +++ b/test-suite/bugs/closed/3685.v @@ -39,11 +39,11 @@ Module Export PointwiseCore. (G : Functor D D') : Functor (C -> D) (C' -> D'). Proof. - refine (Build_Functor + unshelve (refine (Build_Functor (C -> D) (C' -> D') _ _ - _); + _)); abstract admit. Defined. End PointwiseCore. diff --git a/test-suite/bugs/closed/3686.v b/test-suite/bugs/closed/3686.v index b650920b..df5f6674 100644 --- a/test-suite/bugs/closed/3686.v +++ b/test-suite/bugs/closed/3686.v @@ -33,11 +33,11 @@ Module Export PointwiseCore. (G : Functor D D') : Functor (C -> D) (C' -> D'). Proof. - refine (Build_Functor + unshelve (refine (Build_Functor (C -> D) (C' -> D') _ _ - _); + _)); abstract admit. Defined. End PointwiseCore. diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v index df9f5f47..c24173ab 100644 --- a/test-suite/bugs/closed/3690.v +++ b/test-suite/bugs/closed/3690.v @@ -18,7 +18,7 @@ Top.8} Top.6 Top.7 Top.8 |= *) *) -Definition bar := $(let t := eval compute in foo in exact t)$. +Definition bar := ltac:(let t := eval compute in foo in exact t). Check @bar. (* bar@{Top.13 Top.14 Top.15 Top.16} : Type@{Top.16+1} diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v index 62137f0c..aad0bb44 100644 --- a/test-suite/bugs/closed/3699.v +++ b/test-suite/bugs/closed/3699.v @@ -34,8 +34,8 @@ Module NonPrim. : forall b:B, P b. Proof. intros b. - refine (pr1 (isconnected_elim _ _)). - 2:exact b. + unshelve (refine (pr1 (isconnected_elim _ _))). + exact b. intro x. exact (transport P x.2 (d x.1)). Defined. @@ -47,8 +47,8 @@ Module NonPrim. : forall b:B, P b. Proof. intros b. - refine (pr1 (isconnected_elim _ _)). - 2:exact b. + unshelve (refine (pr1 (isconnected_elim _ _))). + exact b. intros [a p]. exact (transport P p (d a)). Defined. @@ -111,8 +111,8 @@ Module Prim. : forall b:B, P b. Proof. intros b. - refine (pr1 (isconnected_elim _ _)). - 2:exact b. + unshelve (refine (pr1 (isconnected_elim _ _))). + exact b. intro x. exact (transport P x.2 (d x.1)). Defined. @@ -124,8 +124,8 @@ Module Prim. : forall b:B, P b. Proof. intros b. - refine (pr1 (isconnected_elim _ _)). - 2:exact b. + unshelve (refine (pr1 (isconnected_elim _ _))). + exact b. intros [a p]. exact (transport P p (d a)). Defined. diff --git a/test-suite/bugs/closed/3735.v b/test-suite/bugs/closed/3735.v new file mode 100644 index 00000000..a50572ac --- /dev/null +++ b/test-suite/bugs/closed/3735.v @@ -0,0 +1,4 @@ +Require Import Coq.Program.Tactics. +Class Foo := { bar : Type }. +Fail Lemma foo : Foo -> bar. (* 'Command has indeed failed.' in both 8.4 and trunk *) +Fail Program Lemma foo : Foo -> bar.
\ No newline at end of file diff --git a/test-suite/bugs/closed/3743.v b/test-suite/bugs/closed/3743.v index 4dfb3380..c799d439 100644 --- a/test-suite/bugs/closed/3743.v +++ b/test-suite/bugs/closed/3743.v @@ -3,7 +3,7 @@ coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (d65496f09c4b68fa318783e53f9cd6d5c18e1eb7) *) Require Export Coq.Setoids.Setoid. -Fail Add Parametric Relation A +Add Parametric Relation A : A (@eq A) transitivity proved by transitivity as refine_rel. diff --git a/test-suite/bugs/closed/3746.v b/test-suite/bugs/closed/3746.v new file mode 100644 index 00000000..a9463f94 --- /dev/null +++ b/test-suite/bugs/closed/3746.v @@ -0,0 +1,92 @@ + +(* Bug report #3746 : Include and restricted signature *) + +Module Type MT. Parameter p : nat. End MT. +Module Type EMPTY. End EMPTY. +Module Empty. End Empty. + +(* Include of an applied functor with restricted sig : + Used to create axioms (bug report #3746), now forbidden. *) + +Module F (X:EMPTY) : MT. + Definition p := 0. +End F. + +Module InclFunctRestr. + Fail Include F(Empty). +End InclFunctRestr. + +(* A few variants (indirect restricted signature), also forbidden. *) + +Module F1 := F. +Module F2 (X:EMPTY) := F X. + +Module F3a (X:EMPTY). Definition p := 0. End F3a. +Module F3 (X:EMPTY) : MT := F3a X. + +Module InclFunctRestrBis. + Fail Include F1(Empty). + Fail Include F2(Empty). + Fail Include F3(Empty). +End InclFunctRestrBis. + +(* Recommended workaround: manual instance before the include. *) + +Module InclWorkaround. + Module Temp := F(Empty). + Include Temp. +End InclWorkaround. + +Compute InclWorkaround.p. +Print InclWorkaround.p. +Print Assumptions InclWorkaround.p. (* Closed under the global context *) + + + +(* Related situations which are ok, just to check *) + +(* A) Include of non-functor with restricted signature : + creates a proxy to initial stuff *) + +Module M : MT. + Definition p := 0. +End M. + +Module InclNonFunct. + Include M. +End InclNonFunct. + +Definition check : InclNonFunct.p = M.p := eq_refl. +Print Assumptions InclNonFunct.p. (* Closed *) + + +(* B) Include of a module type with opaque content: + The opaque content is "copy-pasted". *) + +Module Type SigOpaque. + Definition p : nat. Proof. exact 0. Qed. +End SigOpaque. + +Module InclSigOpaque. + Include SigOpaque. +End InclSigOpaque. + +Compute InclSigOpaque.p. +Print InclSigOpaque.p. +Print Assumptions InclSigOpaque.p. (* Closed *) + + +(* C) Include of an applied functor with opaque proofs : + opaque proof "copy-pasted" (and substituted). *) + +Module F' (X:EMPTY). + Definition p : nat. Proof. exact 0. Qed. +End F'. + +Module InclFunctOpa. + Include F'(Empty). +End InclFunctOpa. + +Compute InclFunctOpa.p. +Print InclFunctOpa.p. +Print Assumptions InclFunctOpa.p. (* Closed *) diff --git a/test-suite/bugs/closed/3807.v b/test-suite/bugs/closed/3807.v new file mode 100644 index 00000000..108ebf59 --- /dev/null +++ b/test-suite/bugs/closed/3807.v @@ -0,0 +1,33 @@ +Set Universe Polymorphism. +Set Printing Universes. +Unset Universe Minimization ToSet. + + +Definition foo : Type := nat. +About foo. +(* foo@{Top.1} : Type@{Top.1}*) +(* Top.1 |= *) + +Definition bar : foo -> nat. +Admitted. +About bar. +(* bar@{Top.2} : foo@{Top.2} -> nat *) +(* Top.2 |= *) + +Lemma baz@{i} : foo@{i} -> nat. +Proof. + exact bar. +Defined. + +Definition bar'@{i} : foo@{i} -> nat. + intros f. exact 0. +Admitted. +About bar'. +(* bar'@{i} : foo@{i} -> nat *) +(* i |= *) + +Axiom f@{i} : Type@{i}. +(* +*** [ f@{i} : Type@{i} ] +(* i |= *) +*)
\ No newline at end of file diff --git a/test-suite/bugs/opened/3848.v b/test-suite/bugs/closed/3848.v index a03e8ffd..c0ef02f1 100644 --- a/test-suite/bugs/opened/3848.v +++ b/test-suite/bugs/closed/3848.v @@ -19,4 +19,4 @@ Proof. refine (functor_forall (f^-1) (fun (x:A) (y:Q (f^-1 x)) => eisretr f x # (g (f^-1 x))^-1 y)). -Fail Defined. (* Error: Attempt to save an incomplete proof *) +Defined. (* was: Error: Attempt to save an incomplete proof *) diff --git a/test-suite/bugs/closed/3881.v b/test-suite/bugs/closed/3881.v index 4408ab88..070d1e9c 100644 --- a/test-suite/bugs/closed/3881.v +++ b/test-suite/bugs/closed/3881.v @@ -8,7 +8,7 @@ Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). Notation "A -> B" := (forall (_ : A), B) : type_scope. Axiom admit : forall {T}, T. Notation "g 'o' f" := (fun x => g (f x)) (at level 40, left associativity). -Notation "g 'o' f" := $(let g' := g in let f' := f in exact (fun x => g' (f' x)))$ (at level 40, left associativity). (* Ensure that x is not captured in [g] or [f] in case they contain holes *) +Notation "g 'o' f" := ltac:(let g' := g in let f' := f in exact (fun x => g' (f' x))) (at level 40, left associativity). (* Ensure that x is not captured in [g] or [f] in case they contain holes *) Inductive eq {A} (x:A) : A -> Prop := eq_refl : x = x where "x = y" := (@eq _ x y) : type_scope. Arguments eq_refl {_ _}. Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with eq_refl => eq_refl end. diff --git a/test-suite/bugs/closed/3923.v b/test-suite/bugs/closed/3923.v new file mode 100644 index 00000000..0aa029e7 --- /dev/null +++ b/test-suite/bugs/closed/3923.v @@ -0,0 +1,33 @@ +Module Type TRIVIAL. +Parameter t:Type. +End TRIVIAL. + +Module MkStore (Key : TRIVIAL). + +Module St : TRIVIAL. +Definition t := unit. +End St. + +End MkStore. + + + +Module Type CERTRUNTIMETYPES (B : TRIVIAL). + +Parameter cert_fieldstore : Type. +Parameter empty_fieldstore : cert_fieldstore. + +End CERTRUNTIMETYPES. + + + +Module MkCertRuntimeTypes (B : TRIVIAL) : CERTRUNTIMETYPES B. + +Module FieldStore := MkStore B. + +Definition cert_fieldstore := FieldStore.St.t. +Axiom empty_fieldstore : cert_fieldstore. + +End MkCertRuntimeTypes. + +Extraction MkCertRuntimeTypes. (* Was leading to an uncaught Not_found *) diff --git a/test-suite/bugs/closed/3998.v b/test-suite/bugs/closed/3998.v new file mode 100644 index 00000000..ced13839 --- /dev/null +++ b/test-suite/bugs/closed/3998.v @@ -0,0 +1,24 @@ +Class FieldType (F : Set) := mkFieldType { fldTy: F -> Set }. +Hint Mode FieldType + : typeclass_instances. (* The F parameter is an input *) + +Inductive I1 := C. +Inductive I2 := . + +Instance I1FieldType : FieldType I1 := { fldTy := I1_rect _ bool }. +Instance I2FieldType : FieldType I2 := { fldTy := I2_rect _ }. + +Definition RecordOf F (FT: FieldType F) := forall f:F, fldTy f. + +Class MapOps (M K : Set) := { + tgtTy: K -> Set; + update: M -> forall k:K, tgtTy k -> M +}. + +Instance RecordMapOps F (FT: FieldType F) : MapOps (RecordOf F FT) F := +{ tgtTy := fldTy; update := fun r (f: F) (x: fldTy f) z => r z }. + +Axiom ex : RecordOf _ I1FieldType. + +Definition works := (fun ex' => update ex' C true) (update ex C false). +Set Typeclasses Debug. +Definition doesnt := update (update ex C false) C true.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4116.v b/test-suite/bugs/closed/4116.v index f808cb45..5932c9c5 100644 --- a/test-suite/bugs/closed/4116.v +++ b/test-suite/bugs/closed/4116.v @@ -110,7 +110,7 @@ Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A. Tactic Notation "transparent" "assert" "(" ident(name) ":" constr(type) ")" := - refine (let __transparent_assert_hypothesis := (_ : type) in _); + unshelve refine (let __transparent_assert_hypothesis := (_ : type) in _); [ | ( let H := match goal with H := _ |- _ => constr:(H) end in @@ -321,7 +321,7 @@ Section Grothendieck. Definition Gcategory : PreCategory. Proof. - refine (@Build_PreCategory + unshelve refine (@Build_PreCategory Pair (fun s d => Gmorphism s d) Gidentity @@ -346,7 +346,7 @@ Section Grothendieck2. Instance iscategory_grothendieck_toset : IsCategory (Gcategory F). Proof. intros s d. - refine (isequiv_adjointify _ _ _ _). + unshelve refine (isequiv_adjointify _ _ _ _). { intro m. transparent assert (H' : (s.(c) = d.(c))). diff --git a/test-suite/bugs/closed/4149.v b/test-suite/bugs/closed/4149.v new file mode 100644 index 00000000..b81c680c --- /dev/null +++ b/test-suite/bugs/closed/4149.v @@ -0,0 +1,4 @@ +Goal forall A, A -> Type. +Proof. + intros; eauto. +Qed. diff --git a/test-suite/bugs/closed/4256.v b/test-suite/bugs/closed/4256.v new file mode 100644 index 00000000..3cdc4ada --- /dev/null +++ b/test-suite/bugs/closed/4256.v @@ -0,0 +1,43 @@ +(* Testing 8.5 regression with type classes not solving evars + redefined while trying to solve them with the type class mechanism *) + +Global Set Universe Polymorphism. +Monomorphic Universe i. +Inductive paths {A : Type} (a : A) : A -> Type := + idpath : paths a a. +Arguments idpath {A a} , [A] a. +Notation "x = y :> A" := (@paths A x y) : type_scope. +Notation "x = y" := (x = y :>_) : type_scope. + +Inductive trunc_index : Type := +| minus_two : trunc_index +| trunc_S : trunc_index -> trunc_index. +Notation "-1" := (trunc_S minus_two) (at level 0). + +Class IsPointed (A : Type) := point : A. +Arguments point A {_}. + +Record pType := + { pointed_type : Type ; + ispointed_type : IsPointed pointed_type }. +Coercion pointed_type : pType >-> Sortclass. +Existing Instance ispointed_type. + +Private Inductive Trunc (n : trunc_index) (A :Type) : Type := + tr : A -> Trunc n A. +Arguments tr {n A} a. + + + +Record ooGroup := + { classifying_space : pType@{i} }. + +Definition group_loops (X : pType) +: ooGroup. +Proof. + (** This works: *) + pose (x0 := point X). + pose (H := existT (fun x:X => Trunc -1 (x = point X)) x0 (tr idpath)). + clear H x0. + (** But this doesn't: *) + pose (existT (fun x:X => Trunc -1 (x = point X)) (point X) (tr idpath)). diff --git a/test-suite/bugs/closed/4273.v b/test-suite/bugs/closed/4273.v new file mode 100644 index 00000000..591ea4b5 --- /dev/null +++ b/test-suite/bugs/closed/4273.v @@ -0,0 +1,9 @@ + + +Set Primitive Projections. +Record total2 (P : nat -> Prop) := tpair { pr1 : nat; pr2 : P pr1 }. +Theorem onefiber' (q : total2 (fun y => y = 0)) : True. +Proof. assert (foo:=pr2 _ q). simpl in foo. + destruct foo. (* Error: q is used in conclusion. *) exact I. Qed. + +Print onefiber'.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4284.v b/test-suite/bugs/closed/4284.v new file mode 100644 index 00000000..0fff3026 --- /dev/null +++ b/test-suite/bugs/closed/4284.v @@ -0,0 +1,6 @@ +Set Primitive Projections. +Record total2 { T: Type } ( P: T -> Type ) := tpair { pr1 : T; pr2 : P pr1 }. +Theorem onefiber' {X : Type} (P : X -> Type) (x : X) : True. +Proof. +set (Q1 := total2 (fun f => pr1 P f = x)). +set (f1:=fun q1 : Q1 => pr2 _ (pr1 _ q1)). diff --git a/test-suite/bugs/closed/4287.v b/test-suite/bugs/closed/4287.v index 0623cf5b..43c9b512 100644 --- a/test-suite/bugs/closed/4287.v +++ b/test-suite/bugs/closed/4287.v @@ -118,8 +118,6 @@ Definition setle (B : Type@{i}) := let foo (A : Type@{j}) := A in foo B. Fail Check @setlt@{j Prop}. -Check @setlt@{Prop j}. -Check @setle@{Prop j}. - Fail Definition foo := @setle@{j Prop}. -Definition foo := @setle@{Prop j}. +Check setlt@{Set i}. +Check setlt@{Set j}.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4293.v b/test-suite/bugs/closed/4293.v new file mode 100644 index 00000000..3671c931 --- /dev/null +++ b/test-suite/bugs/closed/4293.v @@ -0,0 +1,7 @@ +Module Type Foo. +Definition T := let X := Type in Type. +End Foo. + +Module M : Foo. +Definition T := let X := Type in Type. +End M.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4363.v b/test-suite/bugs/closed/4363.v new file mode 100644 index 00000000..9895548c --- /dev/null +++ b/test-suite/bugs/closed/4363.v @@ -0,0 +1,9 @@ +Set Printing Universes. +Definition foo : Type. +Proof. + assert (H : Set) by abstract (assert Type by abstract exact Type using bar; exact nat). + exact bar. +Defined. (* Toplevel input, characters 0-8: +Error: +The term "(fun _ : Set => bar) foo_subproof" has type +"Type@{Top.2}" while it is expected to have type "Type@{Top.1}". *) diff --git a/test-suite/bugs/closed/4400.v b/test-suite/bugs/closed/4400.v new file mode 100644 index 00000000..5c23f840 --- /dev/null +++ b/test-suite/bugs/closed/4400.v @@ -0,0 +1,19 @@ +(* -*- coq-prog-args: ("-emacs" "-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/4404.v b/test-suite/bugs/closed/4404.v new file mode 100644 index 00000000..27b43a61 --- /dev/null +++ b/test-suite/bugs/closed/4404.v @@ -0,0 +1,4 @@ +Inductive Foo : Type -> Type := foo A : Foo A. +Goal True. + remember Foo. + diff --git a/test-suite/bugs/closed/4412.v b/test-suite/bugs/closed/4412.v new file mode 100644 index 00000000..4b2aae0c --- /dev/null +++ b/test-suite/bugs/closed/4412.v @@ -0,0 +1,4 @@ +Require Import Coq.Bool.Bool Coq.Setoids.Setoid. +Goal forall (P : forall b : bool, b = true -> Type) (x y : bool) (H : andb x y = true) (H' : P _ H), True. + intros. + Fail rewrite Bool.andb_true_iff in H. diff --git a/test-suite/bugs/closed/4420.v b/test-suite/bugs/closed/4420.v new file mode 100644 index 00000000..0e16cb23 --- /dev/null +++ b/test-suite/bugs/closed/4420.v @@ -0,0 +1,19 @@ +Module foo. + Context (Char : Type). + Axiom foo : Type -> Type. + Goal foo Char = foo Char. + change foo with (fun x => foo x). + cbv beta. + reflexivity. + Defined. +End foo. + +Inductive foo (A : Type) : Prop := I. (*Top.1*) +Lemma bar : foo Type. (*Top.3*) +Proof. + Set Printing Universes. +change foo with (fun x : Type => foo x). (*Top.4*) +cbv beta. +apply I. (* I Type@{Top.3} : (fun x : Type@{Top.4} => foo x) Type@{Top.3} *) +Defined. + diff --git a/test-suite/bugs/closed/4429.v b/test-suite/bugs/closed/4429.v new file mode 100644 index 00000000..bf0e570a --- /dev/null +++ b/test-suite/bugs/closed/4429.v @@ -0,0 +1,31 @@ +Require Import Arith.Compare_dec. +Require Import Unicode.Utf8. + +Fixpoint my_nat_iter (n : nat) {A} (f : A → A) (x : A) : A := + match n with + | O => x + | S n' => f (my_nat_iter n' f x) + end. + +Definition gcd_IT_F (f : nat * nat → nat) (mn : nat * nat) : nat := + match mn with + | (0, 0) => 0 + | (0, S n') => S n' + | (S m', 0) => S m' + | (S m', S n') => + match le_gt_dec (S m') (S n') with + | left _ => f (S m', S n' - S m') + | right _ => f (S m' - S n', S n') + end + end. + +Axiom max_correct_l : ∀ m n : nat, m <= max m n. +Axiom max_correct_r : ∀ m n : nat, n <= max m n. + +Hint Resolve max_correct_l max_correct_r : arith. + +Theorem foo : ∀ p p' p'' : nat, p'' < S (max p (max p' p'')). +Proof. + intros. + Timeout 3 eauto with arith. +Qed. diff --git a/test-suite/bugs/closed/4433.v b/test-suite/bugs/closed/4433.v new file mode 100644 index 00000000..9eeb8646 --- /dev/null +++ b/test-suite/bugs/closed/4433.v @@ -0,0 +1,29 @@ +Require Import Coq.Arith.Arith Coq.Init.Wf. +Axiom proof_admitted : False. +Goal exists x y z : nat, Fix + Wf_nat.lt_wf + (fun _ => nat -> nat) + (fun x' f => match x' as x'0 + return match x'0 with + | 0 => True + | S x'' => x'' < x' + end + -> nat -> nat + with + | 0 => fun _ _ => 0 + | S x'' => f x'' + end + (match x' with + | 0 => I + | S x'' => (Nat.lt_succ_diag_r _) + end)) + z + y + = 0. +Proof. + do 3 (eexists; [ shelve.. | ]). + match goal with |- ?G => let G' := (eval lazy in G) in change G with G' end. + case proof_admitted. + Unshelve. + all:constructor. +Defined.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4443.v b/test-suite/bugs/closed/4443.v new file mode 100644 index 00000000..66dfa0e6 --- /dev/null +++ b/test-suite/bugs/closed/4443.v @@ -0,0 +1,31 @@ +Set Universe Polymorphism. + +Record TYPE@{i} := cType { + type : Type@{i}; +}. + +Definition PROD@{i j k} + (A : Type@{i}) + (B : A -> Type@{j}) + : TYPE@{k}. +Proof. + refine (cType@{i} _). ++ refine (forall x : A, B x). +Defined. + +Local Unset Strict Universe Declaration. +Definition PRODinj + (A : Type@{i}) + (B : A -> Type) + : TYPE. +Proof. + refine (cType@{i} _). ++ refine (forall x : A, B x). +Defined. + + Monomorphic Universe i j. + Monomorphic Constraint j < i. +Set Printing Universes. +Check PROD@{i i i}. +Check PRODinj@{i j}. +Fail Check PRODinj@{j i}.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4453.v b/test-suite/bugs/closed/4453.v new file mode 100644 index 00000000..009dd5e3 --- /dev/null +++ b/test-suite/bugs/closed/4453.v @@ -0,0 +1,8 @@ + +Section Foo. +Variable A : Type. +Lemma foo : A -> True. now intros _. Qed. +Goal Type -> True. +rename A into B. +intros A. +Fail apply foo. diff --git a/test-suite/bugs/closed/4456.v b/test-suite/bugs/closed/4456.v new file mode 100644 index 00000000..a32acf78 --- /dev/null +++ b/test-suite/bugs/closed/4456.v @@ -0,0 +1,647 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Fiat" "-top" "BooleanRecognizerMin" "-R" "." "Top") -*- *) +(* File reduced by coq-bug-finder from original input, then from 2475 lines to 729 lines, then from 746 lines to 658 lines, then from 675 lines to 658 lines *) +(* coqc version 8.5beta3 (November 2015) compiled on Nov 11 2015 18:23:0 with OCaml 4.01.0 + coqtop version 8.5beta3 (November 2015) *) +(* Variable P : forall n m : nat, n = m -> Prop. *) +(* Axiom Prefl : forall n : nat, P n n eq_refl. *) +Axiom proof_admitted : False. + +Tactic Notation "admit" := case proof_admitted. + +Require Coq.Program.Program. +Require Coq.Strings.String. +Require Coq.omega.Omega. +Module Export Fiat_DOT_Common. +Module Export Fiat. +Module Common. +Import Coq.Lists.List. +Export Coq.Program.Program. + +Global Set Implicit Arguments. + +Global Coercion is_true : bool >-> Sortclass. +Coercion bool_of_sum {A B} (b : sum A B) : bool := if b then true else false. + +Fixpoint ForallT {T} (P : T -> Type) (ls : list T) : Type + := match ls return Type with + | nil => True + | x::xs => (P x * ForallT P xs)%type + end. +Fixpoint Forall_tails {T} (P : list T -> Type) (ls : list T) : Type + := match ls with + | nil => P nil + | x::xs => (P (x::xs) * Forall_tails P xs)%type + end. + +End Common. + +End Fiat. + +End Fiat_DOT_Common. +Module Export Fiat_DOT_Parsers_DOT_StringLike_DOT_Core. +Module Export Fiat. +Module Export Parsers. +Module Export StringLike. +Module Export Core. +Import Coq.Relations.Relation_Definitions. +Import Coq.Classes.Morphisms. + +Local Coercion is_true : bool >-> Sortclass. + +Module Export StringLike. + Class StringLike {Char : Type} := + { + String :> Type; + is_char : String -> Char -> bool; + length : String -> nat; + take : nat -> String -> String; + drop : nat -> String -> String; + get : nat -> String -> option Char; + unsafe_get : nat -> String -> Char; + bool_eq : String -> String -> bool; + beq : relation String := fun x y => bool_eq x y + }. + + Arguments StringLike : clear implicits. + Infix "=s" := (@beq _ _) (at level 70, no associativity) : type_scope. + Notation "s ~= [ ch ]" := (is_char s ch) (at level 70, no associativity) : string_like_scope. + Local Open Scope string_like_scope. + + Class StringLikeProperties (Char : Type) `{StringLike Char} := + { + singleton_unique : forall s ch ch', s ~= [ ch ] -> s ~= [ ch' ] -> ch = ch'; + singleton_exists : forall s, length s = 1 -> exists ch, s ~= [ ch ]; + get_0 : forall s ch, take 1 s ~= [ ch ] <-> get 0 s = Some ch; + get_S : forall n s, get (S n) s = get n (drop 1 s); + unsafe_get_correct : forall n s ch, get n s = Some ch -> unsafe_get n s = ch; + length_singleton : forall s ch, s ~= [ ch ] -> length s = 1; + bool_eq_char : forall s s' ch, s ~= [ ch ] -> s' ~= [ ch ] -> s =s s'; + is_char_Proper :> Proper (beq ==> eq ==> eq) is_char; + length_Proper :> Proper (beq ==> eq) length; + take_Proper :> Proper (eq ==> beq ==> beq) take; + drop_Proper :> Proper (eq ==> beq ==> beq) drop; + bool_eq_Equivalence :> Equivalence beq; + bool_eq_empty : forall str str', length str = 0 -> length str' = 0 -> str =s str'; + take_short_length : forall str n, n <= length str -> length (take n str) = n; + take_long : forall str n, length str <= n -> take n str =s str; + take_take : forall str n m, take n (take m str) =s take (min n m) str; + drop_length : forall str n, length (drop n str) = length str - n; + drop_0 : forall str, drop 0 str =s str; + drop_drop : forall str n m, drop n (drop m str) =s drop (n + m) str; + drop_take : forall str n m, drop n (take m str) =s take (m - n) (drop n str); + take_drop : forall str n m, take n (drop m str) =s drop m (take (n + m) str); + bool_eq_from_get : forall str str', (forall n, get n str = get n str') -> str =s str' + }. +Global Arguments StringLikeProperties _ {_}. +End StringLike. + +End Core. + +End StringLike. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_StringLike_DOT_Core. + +Module Export Fiat_DOT_Parsers_DOT_ContextFreeGrammar_DOT_Core. +Module Export Fiat. +Module Export Parsers. +Module Export ContextFreeGrammar. +Module Export Core. +Import Coq.Strings.String. +Import Coq.Lists.List. +Export Fiat.Parsers.StringLike.Core. + +Section cfg. + Context {Char : Type}. + + Section definitions. + + Inductive item := + | Terminal (_ : Char) + | NonTerminal (_ : string). + + Definition production := list item. + Definition productions := list production. + + Record grammar := + { + Start_symbol :> string; + Lookup :> string -> productions; + Start_productions :> productions := Lookup Start_symbol; + Valid_nonterminals : list string; + Valid_productions : list productions := map Lookup Valid_nonterminals + }. + End definitions. + + End cfg. + +Arguments item _ : clear implicits. +Arguments production _ : clear implicits. +Arguments productions _ : clear implicits. +Arguments grammar _ : clear implicits. + +End Core. + +End ContextFreeGrammar. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_ContextFreeGrammar_DOT_Core. + +Module Export Fiat_DOT_Parsers_DOT_BaseTypes. +Module Export Fiat. +Module Export Parsers. +Module Export BaseTypes. +Import Coq.Arith.Wf_nat. + +Local Coercion is_true : bool >-> Sortclass. + +Section recursive_descent_parser. + Context {Char} {HSL : StringLike Char} {G : grammar Char}. + + Class parser_computational_predataT := + { nonterminals_listT : Type; + nonterminal_carrierT : Type; + of_nonterminal : String.string -> nonterminal_carrierT; + to_nonterminal : nonterminal_carrierT -> String.string; + initial_nonterminals_data : nonterminals_listT; + nonterminals_length : nonterminals_listT -> nat; + is_valid_nonterminal : nonterminals_listT -> nonterminal_carrierT -> bool; + remove_nonterminal : nonterminals_listT -> nonterminal_carrierT -> nonterminals_listT }. + + Class parser_removal_dataT' `{predata : parser_computational_predataT} := + { nonterminals_listT_R : nonterminals_listT -> nonterminals_listT -> Prop + := ltof _ nonterminals_length; + nonterminals_length_zero : forall ls, + nonterminals_length ls = 0 + -> forall nt, is_valid_nonterminal ls nt = false; + remove_nonterminal_dec : forall ls nonterminal, + is_valid_nonterminal ls nonterminal + -> nonterminals_listT_R (remove_nonterminal ls nonterminal) ls; + remove_nonterminal_noninc : forall ls nonterminal, + ~nonterminals_listT_R ls (remove_nonterminal ls nonterminal); + initial_nonterminals_correct : forall nonterminal, + is_valid_nonterminal initial_nonterminals_data (of_nonterminal nonterminal) <-> List.In nonterminal (Valid_nonterminals G); + initial_nonterminals_correct' : forall nonterminal, + is_valid_nonterminal initial_nonterminals_data nonterminal <-> List.In (to_nonterminal nonterminal) (Valid_nonterminals G); + to_of_nonterminal : forall nonterminal, + List.In nonterminal (Valid_nonterminals G) + -> to_nonterminal (of_nonterminal nonterminal) = nonterminal; + of_to_nonterminal : forall nonterminal, + is_valid_nonterminal initial_nonterminals_data nonterminal + -> of_nonterminal (to_nonterminal nonterminal) = nonterminal; + ntl_wf : well_founded nonterminals_listT_R + := well_founded_ltof _ _; + remove_nonterminal_1 + : forall ls ps ps', + is_valid_nonterminal (remove_nonterminal ls ps) ps' + -> is_valid_nonterminal ls ps'; + remove_nonterminal_2 + : forall ls ps ps', + is_valid_nonterminal (remove_nonterminal ls ps) ps' = false + <-> is_valid_nonterminal ls ps' = false \/ ps = ps' }. + + Class split_dataT := + { split_string_for_production + : item Char -> production Char -> String -> list nat }. + + Class boolean_parser_dataT := + { predata :> parser_computational_predataT; + split_data :> split_dataT }. +End recursive_descent_parser. + +End BaseTypes. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_BaseTypes. + +Module Export Fiat_DOT_Common_DOT_List_DOT_Operations. +Module Export Fiat. +Module Export Common. +Module Export List. +Module Export Operations. + +Import Coq.Lists.List. + +Module Export List. + Section InT. + Context {A : Type} (a : A). + + Fixpoint InT (ls : list A) : Set + := match ls return Set with + | nil => False + | b :: m => (b = a) + InT m + end%type. + End InT. + + End List. + +End Operations. + +End List. + +End Common. + +End Fiat. + +End Fiat_DOT_Common_DOT_List_DOT_Operations. + +Module Export Fiat_DOT_Parsers_DOT_StringLike_DOT_Properties. +Module Export Fiat. +Module Export Parsers. +Module Export StringLike. +Module Export Properties. + +Section String. + Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char}. + + Lemma take_length {str n} + : length (take n str) = min n (length str). +admit. +Defined. + + End String. + +End Properties. + +End StringLike. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_StringLike_DOT_Properties. + +Module Export Fiat_DOT_Parsers_DOT_ContextFreeGrammar_DOT_Properties. +Module Export Fiat. +Module Export Parsers. +Module Export ContextFreeGrammar. +Module Export Properties. + +Local Open Scope list_scope. +Definition production_is_reachableT {Char} (G : grammar Char) (p : production Char) + := { nt : _ + & { prefix : _ + & List.In nt (Valid_nonterminals G) + * List.InT + (prefix ++ p) + (Lookup G nt) } }%type. + +End Properties. + +End ContextFreeGrammar. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_ContextFreeGrammar_DOT_Properties. + +Module Export Fiat_DOT_Parsers_DOT_MinimalParse. +Module Export Fiat. +Module Export Parsers. +Module Export MinimalParse. +Import Coq.Lists.List. +Import Fiat.Parsers.ContextFreeGrammar.Core. + +Local Coercion is_true : bool >-> Sortclass. +Local Open Scope string_like_scope. + +Section cfg. + Context {Char} {HSL : StringLike Char} {G : grammar Char}. + Context {predata : @parser_computational_predataT} + {rdata' : @parser_removal_dataT' _ G predata}. + + Inductive minimal_parse_of + : forall (len0 : nat) (valid : nonterminals_listT) + (str : String), + productions Char -> Type := + | MinParseHead : forall len0 valid str pat pats, + @minimal_parse_of_production len0 valid str pat + -> @minimal_parse_of len0 valid str (pat::pats) + | MinParseTail : forall len0 valid str pat pats, + @minimal_parse_of len0 valid str pats + -> @minimal_parse_of len0 valid str (pat::pats) + with minimal_parse_of_production + : forall (len0 : nat) (valid : nonterminals_listT) + (str : String), + production Char -> Type := + | MinParseProductionNil : forall len0 valid str, + length str = 0 + -> @minimal_parse_of_production len0 valid str nil + | MinParseProductionCons : forall len0 valid str n pat pats, + length str <= len0 + -> @minimal_parse_of_item len0 valid (take n str) pat + -> @minimal_parse_of_production len0 valid (drop n str) pats + -> @minimal_parse_of_production len0 valid str (pat::pats) + with minimal_parse_of_item + : forall (len0 : nat) (valid : nonterminals_listT) + (str : String), + item Char -> Type := + | MinParseTerminal : forall len0 valid str ch, + str ~= [ ch ] + -> @minimal_parse_of_item len0 valid str (Terminal ch) + | MinParseNonTerminal + : forall len0 valid str (nt : String.string), + @minimal_parse_of_nonterminal len0 valid str nt + -> @minimal_parse_of_item len0 valid str (NonTerminal nt) + with minimal_parse_of_nonterminal + : forall (len0 : nat) (valid : nonterminals_listT) + (str : String), + String.string -> Type := + | MinParseNonTerminalStrLt + : forall len0 valid (nt : String.string) str, + length str < len0 + -> is_valid_nonterminal initial_nonterminals_data (of_nonterminal nt) + -> @minimal_parse_of (length str) initial_nonterminals_data str (Lookup G nt) + -> @minimal_parse_of_nonterminal len0 valid str nt + | MinParseNonTerminalStrEq + : forall len0 str valid nonterminal, + length str = len0 + -> is_valid_nonterminal initial_nonterminals_data (of_nonterminal nonterminal) + -> is_valid_nonterminal valid (of_nonterminal nonterminal) + -> @minimal_parse_of len0 (remove_nonterminal valid (of_nonterminal nonterminal)) str (Lookup G nonterminal) + -> @minimal_parse_of_nonterminal len0 valid str nonterminal. + +End cfg. + +End MinimalParse. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_MinimalParse. + +Module Export Fiat_DOT_Parsers_DOT_CorrectnessBaseTypes. +Module Export Fiat. +Module Export Parsers. +Module Export CorrectnessBaseTypes. +Import Coq.Lists.List. +Import Fiat.Parsers.ContextFreeGrammar.Core. +Import Fiat_DOT_Common.Fiat.Common. +Section general. + Context {Char} {HSL : StringLike Char} {G : grammar Char}. + + Definition split_list_completeT_for {data : @parser_computational_predataT} + {len0 valid} + (it : item Char) (its : production Char) + (str : String) + (pf : length str <= len0) + (split_list : list nat) + + := ({ n : nat + & (minimal_parse_of_item (G := G) (predata := data) len0 valid (take n str) it) + * (minimal_parse_of_production (G := G) len0 valid (drop n str) its) }%type) + -> ({ n : nat + & (In (min (length str) n) (map (min (length str)) split_list)) + * (minimal_parse_of_item (G := G) len0 valid (take n str) it) + * (minimal_parse_of_production (G := G) len0 valid (drop n str) its) }%type). + + Definition split_list_completeT {data : @parser_computational_predataT} + (splits : item Char -> production Char -> String -> list nat) + := forall len0 valid str (pf : length str <= len0) nt, + is_valid_nonterminal initial_nonterminals_data (of_nonterminal nt) + -> ForallT + (Forall_tails + (fun prod + => match prod return Type with + | nil => True + | it::its + => @split_list_completeT_for data len0 valid it its str pf (splits it its str) + end)) + (Lookup G nt). + + Class boolean_parser_completeness_dataT' {data : boolean_parser_dataT} := + { split_string_for_production_complete + : split_list_completeT split_string_for_production }. +End general. + +End CorrectnessBaseTypes. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_CorrectnessBaseTypes. + +Module Export Fiat. +Module Export Parsers. +Module Export ContextFreeGrammar. +Module Export Valid. +Export Fiat.Parsers.StringLike.Core. + +Section cfg. + Context {Char : Type} {HSL : StringLike Char} (G : grammar Char) + {predata : parser_computational_predataT}. + + Definition item_valid (it : item Char) + := match it with + | Terminal _ => True + | NonTerminal nt' => is_true (is_valid_nonterminal initial_nonterminals_data (of_nonterminal nt')) + end. + + Definition production_valid pat + := List.Forall item_valid pat. + + Definition productions_valid pats + := List.Forall production_valid pats. + + Definition grammar_valid + := forall nt, + List.In nt (Valid_nonterminals G) + -> productions_valid (Lookup G nt). +End cfg. + +End Valid. + +Section app. + Context {Char : Type} {HSL : StringLike Char} (G : grammar Char) + {predata : parser_computational_predataT}. + + Lemma hd_production_valid + (it : item Char) + (its : production Char) + (H : production_valid (it :: its)) + : item_valid it. +admit. +Defined. + + Lemma production_valid_cons + (it : item Char) + (its : production Char) + (H : production_valid (it :: its)) + : production_valid its. +admit. +Defined. + + End app. + +Import Coq.Lists.List. +Import Coq.omega.Omega. +Import Fiat_DOT_Common.Fiat.Common. +Import Fiat.Parsers.ContextFreeGrammar.Valid. +Local Open Scope string_like_scope. + +Section recursive_descent_parser. + Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char} (G : grammar Char). + Context {data : @boolean_parser_dataT Char _} + {cdata : @boolean_parser_completeness_dataT' Char _ G data} + {rdata : @parser_removal_dataT' _ G _} + {gvalid : grammar_valid G}. + + Local Notation dec T := (T + (T -> False))%type (only parsing). + + Local Notation iffT x y := ((x -> y) * (y -> x))%type (only parsing). + + Lemma dec_prod {A B} (HA : dec A) (HB : dec B) : dec (A * B). +admit. +Defined. + + Lemma dec_In {A} {P : A -> Type} (HA : forall a, dec (P a)) ls + : dec { a : _ & (In a ls * P a) }. +admit. +Defined. + + Section item. + Context {len0 valid} + (str : String) + (str_matches_nonterminal' + : nonterminal_carrierT -> bool) + (str_matches_nonterminal + : forall nt : nonterminal_carrierT, + dec (minimal_parse_of_nonterminal (G := G) len0 valid str (to_nonterminal nt))). + + Section valid. + Context (Hmatches + : forall nt, + is_valid_nonterminal initial_nonterminals_data nt + -> str_matches_nonterminal nt = str_matches_nonterminal' nt :> bool) + (it : item Char) + (Hvalid : item_valid it). + + Definition parse_item' + : dec (minimal_parse_of_item (G := G) len0 valid str it). + Proof. + clear Hvalid. + refine (match it return dec (minimal_parse_of_item len0 valid str it) with + | Terminal ch => if Sumbool.sumbool_of_bool (str ~= [ ch ]) + then inl (MinParseTerminal _ _ _ _ _) + else inr (fun _ => !) + | NonTerminal nt => if str_matches_nonterminal (of_nonterminal nt) + then inl (MinParseNonTerminal _) + else inr (fun _ => !) + end); + clear str_matches_nonterminal Hmatches; + admit. + Defined. + End valid. + + End item. + Context {len0 valid} + (parse_nonterminal + : forall (str : String) (len : nat) (Hlen : length str = len) (pf : len <= len0) (nt : nonterminal_carrierT), + dec (minimal_parse_of_nonterminal (G := G) len0 valid str (to_nonterminal nt))). + + Lemma dec_in_helper {ls it its str} + : iffT {n0 : nat & + (In (min (length str) n0) (map (min (length str)) ls) * + minimal_parse_of_item (G := G) len0 valid (take n0 str) it * + minimal_parse_of_production (G := G) len0 valid (drop n0 str) its)%type} + {n0 : nat & + (In n0 ls * + (minimal_parse_of_item (G := G) len0 valid (take n0 str) it * + minimal_parse_of_production (G := G) len0 valid (drop n0 str) its))%type}. +admit. +Defined. + + Lemma parse_production'_helper {str it its} (pf : length str <= len0) + : dec {n0 : nat & + (minimal_parse_of_item (G := G) len0 valid (take n0 str) it * + minimal_parse_of_production (G := G) len0 valid (drop n0 str) its)%type} + -> dec (minimal_parse_of_production (G := G) len0 valid str (it :: its)). +admit. +Defined. + Local Ltac t_parse_production_for := repeat + match goal with + | [ H : (beq_nat _ _) = true |- _ ] => apply EqNat.beq_nat_true in H + | _ => progress subst + | _ => solve [ constructor; assumption ] + | [ H : minimal_parse_of_production _ _ _ nil |- _ ] => (inversion H; clear H) + | [ H : minimal_parse_of_production _ _ _ (_::_) |- _ ] => (inversion H; clear H) + | [ H : ?x = 0, H' : context[?x] |- _ ] => rewrite H in H' + | _ => progress simpl in * + | _ => discriminate + | [ H : forall x, (_ * _)%type -> _ |- _ ] => specialize (fun x y z => H x (y, z)) + | _ => solve [ eauto with nocore ] + | _ => solve [ apply Min.min_case_strong; omega ] + | _ => omega + | [ H : production_valid (_::_) |- _ ] + => let H' := fresh in + pose proof H as H'; + apply production_valid_cons in H; + apply hd_production_valid in H' + end. + + Definition parse_production'_for + (splits : item Char -> production Char -> String -> list nat) + (Hsplits : forall str it its (Hreachable : production_is_reachableT G (it::its)) pf', split_list_completeT_for (len0 := len0) (G := G) (valid := valid) it its str pf' (splits it its str)) + (str : String) + (len : nat) + (Hlen : length str = len) + (pf : len <= len0) + (prod : production Char) + (Hreachable : production_is_reachableT G prod) + : dec (minimal_parse_of_production (G := G) len0 valid str prod). + Proof. + revert prod Hreachable str len Hlen pf. + refine + ((fun pf_helper => + list_rect + (fun prod => + forall (Hreachable : production_is_reachableT G prod) + (str : String) + (len : nat) + (Hlen : length str = len) + (pf : len <= len0), + dec (minimal_parse_of_production (G := G) len0 valid str prod)) + ( + fun Hreachable str len Hlen pf + => match Utils.dec (beq_nat len 0) with + | left H => inl _ + | right H => inr (fun p => _) + end) + (fun it its parse_production' Hreachable str len Hlen pf + => parse_production'_helper + _ + (let parse_item := (fun n pf => parse_item' (parse_nonterminal (take n str) (len := min n len) (eq_trans take_length (f_equal (min _) Hlen)) pf) it) in + let parse_item := (fun n => parse_item n (Min.min_case_strong n len (fun k => k <= len0) (fun Hlen => (Nat.le_trans _ _ _ Hlen pf)) (fun Hlen => pf))) in + let parse_production := (fun n => parse_production' (pf_helper it its Hreachable) (drop n str) (len - n) (eq_trans (drop_length _ _) (f_equal (fun x => x - _) Hlen)) (Nat.le_trans _ _ _ (Nat.le_sub_l _ _) pf)) in + match dec_In + (fun n => dec_prod (parse_item n) (parse_production n)) + (splits it its str) + with + | inl p => inl (existT _ (projT1 p) (snd (projT2 p))) + | inr p + => let pf' := (Nat.le_trans _ _ _ (Nat.eq_le_incl _ _ Hlen) pf) in + let H := (_ : split_list_completeT_for (G := G) (len0 := len0) (valid := valid) it its str pf' (splits it its str)) in + inr (fun p' => p (fst dec_in_helper (H p'))) + end) + )) _); + [ clear parse_nonterminal Hsplits splits rdata cdata + | clear parse_nonterminal Hsplits splits rdata cdata + | .. + | admit ]. + abstract t_parse_production_for. + abstract t_parse_production_for. + abstract t_parse_production_for. + abstract t_parse_production_for. + Defined. diff --git a/test-suite/bugs/closed/4462.v b/test-suite/bugs/closed/4462.v new file mode 100644 index 00000000..c680518c --- /dev/null +++ b/test-suite/bugs/closed/4462.v @@ -0,0 +1,7 @@ +Variables P Q : Prop. +Axiom pqrw : P <-> Q. + +Require Setoid. + +Goal P -> Q. +unshelve (rewrite pqrw). diff --git a/test-suite/bugs/closed/4467.v b/test-suite/bugs/closed/4467.v new file mode 100644 index 00000000..6f8631d4 --- /dev/null +++ b/test-suite/bugs/closed/4467.v @@ -0,0 +1,15 @@ +(* Fixing missing test for variable shadowing *) + +Definition test (x y:bool*bool) := + match x with + | (e as e1, (true) as e2) + | ((true) as e1, e as e2) => + let '(e, b) := y in + e + | _ => true + end. + +Goal test (true,false) (true,true) = true. +(* used to evaluate to "false = true" in 8.4 *) +reflexivity. +Qed. diff --git a/test-suite/bugs/closed/4480.v b/test-suite/bugs/closed/4480.v new file mode 100644 index 00000000..08a86330 --- /dev/null +++ b/test-suite/bugs/closed/4480.v @@ -0,0 +1,12 @@ +Require Import Setoid. + +Definition proj (P Q : Prop) := P. + +Lemma foo (P : Prop) : proj P P = P. +Admitted. +Lemma trueI : True <-> True. +Admitted. +Goal True. + Fail setoid_rewrite foo. + Fail setoid_rewrite trueI. +
\ No newline at end of file diff --git a/test-suite/bugs/closed/4484.v b/test-suite/bugs/closed/4484.v new file mode 100644 index 00000000..f988539d --- /dev/null +++ b/test-suite/bugs/closed/4484.v @@ -0,0 +1,10 @@ +(* Testing 8.5 regression with type classes not solving evars + redefined while trying to solve them with the type class mechanism *) + +Class A := {}. +Axiom foo : forall {ac : A}, bool. +Lemma bar (ac : A) : True. +Check (match foo as k return foo = k -> True with + | true => _ + | false => _ + end eq_refl). diff --git a/test-suite/bugs/closed/931.v b/test-suite/bugs/closed/931.v index e86b3be6..ea3347a8 100644 --- a/test-suite/bugs/closed/931.v +++ b/test-suite/bugs/closed/931.v @@ -2,6 +2,6 @@ Parameter P : forall n : nat, n=n -> Prop. Goal Prop. refine (P _ _). - 2:instantiate (1:=0). + instantiate (1:=0). trivial. Qed. diff --git a/test-suite/bugs/closed/HoTT_coq_077.v b/test-suite/bugs/closed/HoTT_coq_077.v index db3b60ed..017780c1 100644 --- a/test-suite/bugs/closed/HoTT_coq_077.v +++ b/test-suite/bugs/closed/HoTT_coq_077.v @@ -30,7 +30,7 @@ Definition prod_rect' A B (P : prod A B -> Type) (u : forall (fst : A) (snd : B) (p : prod A B) : P p := u (fst p) (snd p). -Notation typeof x := ($(let T := type of x in exact T)$) (only parsing). +Notation typeof x := (ltac:(let T := type of x in exact T)) (only parsing). (* Check for eta *) Check eq_refl : typeof (@prod_rect) = typeof (@prod_rect'). diff --git a/test-suite/bugs/closed/HoTT_coq_090.v b/test-suite/bugs/closed/HoTT_coq_090.v index 5fa16703..d77b9b63 100644 --- a/test-suite/bugs/closed/HoTT_coq_090.v +++ b/test-suite/bugs/closed/HoTT_coq_090.v @@ -84,7 +84,7 @@ Arguments transport {A} P {x y} p%path_scope u : simpl nomatch. Instance isequiv_path {A B : Type} (p : A = B) : IsEquiv (transport (fun X:Type => X) p) | 0. Proof. - refine (@BuildIsEquiv _ _ _ (transport (fun X:Type => X) p^) _ _ _); + unshelve refine (@BuildIsEquiv _ _ _ (transport (fun X:Type => X) p^) _ _ _); admit. Defined. diff --git a/test-suite/bugs/closed/HoTT_coq_114.v b/test-suite/bugs/closed/HoTT_coq_114.v index 34112833..3535e6c4 100644 --- a/test-suite/bugs/closed/HoTT_coq_114.v +++ b/test-suite/bugs/closed/HoTT_coq_114.v @@ -1 +1 @@ -Inductive test : $(let U := type of Type in exact U)$ := t. +Inductive test : ltac:(let U := type of Type in exact U) := t. diff --git a/test-suite/bugs/opened/3248.v b/test-suite/bugs/opened/3248.v index 9e7d1eb5..33c408a2 100644 --- a/test-suite/bugs/opened/3248.v +++ b/test-suite/bugs/opened/3248.v @@ -3,7 +3,7 @@ Ltac ret_and_left f := let T := type of f in lazymatch eval hnf in T with | ?T' -> _ => - let ret := constr:(fun x' : T' => $(tac (f x'))$) in + let ret := constr:(fun x' : T' => ltac:(tac (f x'))) in exact ret | ?T' => exact f end. @@ -12,6 +12,6 @@ Goal forall A B : Prop, forall x y : A, True. Proof. intros A B x y. pose (f := fun (x y : A) => conj x y). - pose (a := $(ret_and_left f)$). + pose (a := ltac:(ret_and_left f)). Fail unify (a x y) (conj x y). Abort. diff --git a/test-suite/bugs/opened/3277.v b/test-suite/bugs/opened/3277.v index 19ed787d..5f423136 100644 --- a/test-suite/bugs/opened/3277.v +++ b/test-suite/bugs/opened/3277.v @@ -4,4 +4,4 @@ Goal True. evarr _. Admitted. Goal True. - Fail exact $(evarr _)$. (* Error: Cannot infer this placeholder. *) + Fail exact ltac:(evarr _). (* Error: Cannot infer this placeholder. *) diff --git a/test-suite/bugs/opened/3278.v b/test-suite/bugs/opened/3278.v index ced535af..1c6deae9 100644 --- a/test-suite/bugs/opened/3278.v +++ b/test-suite/bugs/opened/3278.v @@ -1,8 +1,8 @@ Module a. Check let x' := _ in - $(exact x')$. + ltac:(exact x'). - Notation foo x := (let x' := x in $(exact x')$). + Notation foo x := (let x' := x in ltac:(exact x')). Fail Check foo _. (* Error: Cannot infer an internal placeholder of type "Type" in environment: @@ -12,10 +12,10 @@ x' := ?42 : ?41 End a. Module b. - Notation foo x := (let x' := x in let y := ($(exact I)$ : True) in I). + Notation foo x := (let x' := x in let y := (ltac:(exact I) : True) in I). Notation bar x := (let x' := x in let y := (I : True) in I). - Check let x' := _ in $(exact I)$. (* let x' := ?5 in I *) + Check let x' := _ in ltac:(exact I). (* let x' := ?5 in I *) Check bar _. (* let x' := ?9 in let y := I in I *) Fail Check foo _. (* Error: Cannot infer an internal placeholder of type "Type" in environment: diff --git a/test-suite/bugs/opened/3304.v b/test-suite/bugs/opened/3304.v index 529cc737..66668930 100644 --- a/test-suite/bugs/opened/3304.v +++ b/test-suite/bugs/opened/3304.v @@ -1,3 +1,3 @@ -Fail Notation "( x , y , .. , z )" := $(let r := constr:(prod .. (prod x y) .. z) in r)$. +Fail Notation "( x , y , .. , z )" := ltac:(let r := constr:(prod .. (prod x y) .. z) in r). (* The command has indeed failed with message: => Error: Special token .. is for use in the Notation command. *) diff --git a/test-suite/bugs/opened/3459.v b/test-suite/bugs/opened/3459.v index 9e6107b3..762611f7 100644 --- a/test-suite/bugs/opened/3459.v +++ b/test-suite/bugs/opened/3459.v @@ -7,9 +7,9 @@ Proof. (* This line used to fail with a Not_found up to some point, and then to produce an ill-typed term *) match goal with - | [ |- context G[2] ] => let y := constr:(fun x => $(let r := constr:(@eq Set x x) in + | [ |- context G[2] ] => let y := constr:(fun x => ltac:(let r := constr:(@eq Set x x) in clear x; - exact r)$) in + exact r)) in pose y end. (* Add extra test for typability (should not fail when bug closed) *) diff --git a/test-suite/bugs/opened/3554.v b/test-suite/bugs/opened/3554.v deleted file mode 100644 index 422c5770..00000000 --- a/test-suite/bugs/opened/3554.v +++ /dev/null @@ -1 +0,0 @@ -Fail Example foo (f : forall {_ : Type}, Type) : Type. diff --git a/test-suite/complexity/f_equal.v b/test-suite/complexity/f_equal.v new file mode 100644 index 00000000..86698fa8 --- /dev/null +++ b/test-suite/complexity/f_equal.v @@ -0,0 +1,14 @@ +(* Checks that f_equal does not reduce the term uselessly *) +(* Expected time < 1.00s *) + +Fixpoint stupid (n : nat) : unit := +match n with +| 0 => tt +| S n => + let () := stupid n in + let () := stupid n in + tt +end. + +Goal stupid 23 = stupid 23. +Timeout 5 Time f_equal. diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v index 749db000..d91d159d 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-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \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 8e34ffbd..b3fbff68 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-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \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 7b52316e..c2b521c2 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-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \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 b3a0a335..8db27858 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-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \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 7e4c5ac5..8ed3af1c 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-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v index d44bccdf..91de8733 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-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \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 e5db8176..c8dc6303 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-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \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 a6e6bc48..648ab082 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-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ideal-features/Apply.v b/test-suite/ideal-features/Apply.v index ed46eb22..c8e9af21 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-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/misc/berardi_test.v b/test-suite/misc/berardi_test.v index 219686b9..a64db4da 100644 --- a/test-suite/misc/berardi_test.v +++ b/test-suite/misc/berardi_test.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/output/Existentials.out b/test-suite/output/Existentials.out index 483a9ea7..52e1e0ed 100644 --- a/test-suite/output/Existentials.out +++ b/test-suite/output/Existentials.out @@ -1,5 +1,5 @@ Existential 1 = -?Goal0 : [p : nat q := S p : nat n : nat m : nat |- ?y = m] +?Goal1 : [p : nat q := S p : nat n : nat m : nat |- ?y = m] Existential 2 = ?y : [p : nat q := S p : nat n : nat m : nat |- nat] (p, q cannot be used) -Existential 3 = ?e : [q : nat n : nat m : nat |- n = ?y] +Existential 3 = ?Goal0 : [q : nat n : nat m : nat |- n = ?y] diff --git a/test-suite/output/Extraction_matchs_2413.out b/test-suite/output/Extraction_matchs_2413.out index 848abd00..f738b0d0 100644 --- a/test-suite/output/Extraction_matchs_2413.out +++ b/test-suite/output/Extraction_matchs_2413.out @@ -4,7 +4,7 @@ let test1 b = b (** val test2 : bool -> bool **) -let test2 b = +let test2 _ = False (** val wrong_id : 'a1 hole -> 'a2 hole **) diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v index ce9050d4..3c696502 100644 --- a/test-suite/success/Case22.v +++ b/test-suite/success/Case22.v @@ -17,3 +17,47 @@ Definition foo (x : I') : bool := match x with C' => true end. + +(* Bug found in november 2015: was wrongly failing in 8.5beta2 and 8.5beta3 *) + +Inductive I2 (A:Type) : let B:=A in forall C, let D:=(C*B)%type in Type := + E2 : I2 A nat. + +Check fun x:I2 nat nat => match x in I2 _ X Y Z return X*Y*Z with + E2 _ => (0,0,(0,0)) + end. + +(* This used to succeed in 8.3, 8.4 and 8.5beta1 *) + +Inductive IND : forall X:Type, let Y:=X in Type := + CONSTR : IND True. + +Definition F (x:IND True) (A:Type) := + (* This failed in 8.5beta2 though it should have been accepted *) + match x in IND X Y return Y with + CONSTR => Logic.I + end. + +Theorem paradox : False. + (* This succeeded in 8.3, 8.4 and 8.5beta1 because F had wrong type *) +Fail Proof (F C False). + +(* Another bug found in November 2015 (a substitution was wrongly + reversed at pretyping level) *) + +Inductive Ind (A:Type) : + let X:=A in forall Y:Type, let Z:=(X*Y)%type in Type := + Constr : Ind A nat. + +Check fun x:Ind bool nat => + match x in Ind _ X Y Z return Z with + | Constr _ => (true,0) + end. + +(* A vm_compute bug (the type of constructors was not supposed to + contain local definitions before proper parameters) *) + +Inductive Ind2 (b:=1) (c:nat) : Type := + Constr2 : Ind2 c. + +Eval vm_compute in Constr2 2. diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index e4266350..49c465b6 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -1861,3 +1861,10 @@ Type (fun n => match n with Definition transport {A} (P : A->Type) {x y : A} (p : x=y) (u : P x) : P y := match p with eq_refl => u end. + +(* Check in-pattern clauses with constant constructors, which were + previously interpreted as variables (before 8.5) *) + +Check match eq_refl 0 in _=O return O=O with eq_refl => eq_refl end. + +Check match niln in listn O return O=O with niln => eq_refl end. diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v index 87c38cfa..e4ee351c 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-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v index 8db08b6d..438e4613 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-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 2371d32c..b72a0674 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -101,3 +101,9 @@ Fail Check fun x => match x with S (FORALL x, _) => 0 end. Parameter traverse : (nat -> unit) -> (nat -> unit). Notation traverse_var f l := (traverse (fun l => f l) l). + +(* Check that when an ident become a keyword, it does not break + previous rules relying on the string to be classified as an ident *) + +Notation "'intros' x" := (S x) (at level 0). +Goal True -> True. intros H. exact H. Qed. diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v index 01d9afb4..767f15be 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-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \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 3090f40c..c8a8b862 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-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 83a33f75..9f091e39 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -97,6 +97,7 @@ Abort. Goal exists x, S x = S 0. eexists. +Show x. (* Incidentally test Show on a named goal *) destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *) change (0 = S 0). Abort. @@ -105,6 +106,7 @@ Goal exists x, S 0 = S x. eexists. destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *) change (0 = S ?x). +[x]: exact 0. (* Incidentally test applying a tactic to a goal on the shelve *) Abort. Goal exists n p:nat, (S n,S n) = (S p,S p) /\ p = n. @@ -387,7 +389,7 @@ Abort. Goal forall b:bool, True. intro b. -destruct !b. +destruct (b). clear b. (* b has to be here *) Abort. diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v index 9e57801e..773dd321 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-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \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 1b5c7f18..1f6af0dc 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-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \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 57f3775d..0086e090 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \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_impl.v b/test-suite/success/extraction_impl.v new file mode 100644 index 00000000..dfdeff82 --- /dev/null +++ b/test-suite/success/extraction_impl.v @@ -0,0 +1,82 @@ + +(** Examples of extraction with manually-declared implicit arguments *) + +(** NB: we should someday check the produced code instead of + simply running the commands. *) + +(** Bug #4243, part 1 *) + +Inductive dnat : nat -> Type := +| d0 : dnat 0 +| ds : forall n m, n = m -> dnat n -> dnat (S n). + +Extraction Implicit ds [m]. + +Lemma dnat_nat: forall n, dnat n -> nat. +Proof. + intros n d. + induction d as [| n m Heq d IHn]. + exact 0. exact (S IHn). +Defined. + +Recursive Extraction dnat_nat. + +Extraction Implicit dnat_nat [n]. +Recursive Extraction dnat_nat. + +(** Same, with a Fixpoint *) + +Fixpoint dnat_nat' n (d:dnat n) := + match d with + | d0 => 0 + | ds n m _ d => S (dnat_nat' n d) + end. + +Recursive Extraction dnat_nat'. + +Extraction Implicit dnat_nat' [n]. +Recursive Extraction dnat_nat'. + +(** Bug #4243, part 2 *) + +Inductive enat: nat -> Type := + e0: enat 0 +| es: forall n, enat n -> enat (S n). + +Lemma enat_nat: forall n, enat n -> nat. +Proof. + intros n e. + induction e as [| n e IHe]. + exact (O). + exact (S IHe). +Defined. + +Extraction Implicit es [n]. +Extraction Implicit enat_nat [n]. +Recursive Extraction enat_nat. + +(** Same, with a Fixpoint *) + +Fixpoint enat_nat' n (e:enat n) : nat := + match e with + | e0 => 0 + | es n e => S (enat_nat' n e) + end. + +Extraction Implicit enat_nat' [n]. +Recursive Extraction enat_nat'. + +(** Bug #4228 *) + +Module Food. +Inductive Course := +| main: nat -> Course +| dessert: nat -> Course. + +Inductive Meal : Course -> Type := +| one_course : forall n:nat, Meal (main n) +| two_course : forall n m, Meal (main n) -> Meal (dessert m). +Extraction Implicit two_course [n]. +End Food. + +Recursive Extraction Food.Meal. diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v index b733aef6..c729b23c 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-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \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 7ae60d98..b8c6bf3f 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-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index 35ba94fb..11156aa0 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -34,38 +34,53 @@ intros _ ?. exact H. Qed. -(* A short test about introduction pattern pat/c *) +(* A short test about introduction pattern pat%c *) Goal (True -> 0=0) -> True /\ False -> 0=0. -intros H (H1/H,_). +intros H (H1%H,_). exact H1. Qed. (* A test about bugs in 8.5beta2 *) Goal (True -> 0=0) -> True /\ False -> False -> 0=0. intros H H0 H1. -destruct H0 as (a/H,_). +destruct H0 as (a%H,_). (* Check that H0 is removed (was bugged in 8.5beta2) *) Fail clear H0. -(* Check position of newly created hypotheses when using pat/c (was +(* Check position of newly created hypotheses when using pat%c (was left at top in 8.5beta2) *) match goal with H:_ |- _ => clear H end. (* clear H1:False *) match goal with H:_ |- _ => exact H end. (* check that next hyp shows 0=0 *) Qed. Goal (True -> 0=0) -> True -> 0=0. -intros H H1/H. +intros H H1%H. exact H1. Qed. Goal forall n, n = S n -> 0=0. -intros n H/n_Sn. +intros n H%n_Sn. destruct H. Qed. (* Another check about generated names and cleared hypotheses with - pat/c patterns *) + pat%c patterns *) Goal (True -> 0=0 /\ 1=1) -> True -> 0=0. -intros H (H1,?)/H. +intros H (H1,?)%H. change (1=1) in H0. exact H1. Qed. + +(* Checking iterated pat%c1...%cn introduction patterns and side conditions *) + +Goal forall A B C D:Prop, (A -> B -> C) -> (C -> D) -> B -> A -> D. +intros * H H0 H1. +intros H2%H%H0. +- exact H2. +- exact H1. +Qed. + +(* Bug found by Enrico *) + +Goal forall x : nat, True. +intros y%(fun x => x). +Abort. diff --git a/test-suite/success/keyedrewrite.v b/test-suite/success/keyedrewrite.v index bbe9d4bf..5b0502cf 100644 --- a/test-suite/success/keyedrewrite.v +++ b/test-suite/success/keyedrewrite.v @@ -22,3 +22,40 @@ Qed. Print Equivalent Keys. End foo. + +Require Import Arith List Omega. + +Definition G {A} (f : A -> A -> A) (x : A) := f x x. + +Lemma list_foo A (l : list A) : G (@app A) (l ++ nil) = G (@app A) l. +Proof. unfold G; rewrite app_nil_r; reflexivity. Qed. + +(* Bundled version of a magma *) +Structure magma := Magma { b_car :> Type; op : b_car -> b_car -> b_car }. +Arguments op {_} _ _. + +(* Instance for lists *) +Canonical Structure list_magma A := Magma (list A) (@app A). + +(* Basically like list_foo, but now uses the op projection instead of app for +the argument of G *) +Lemma test1 A (l : list A) : G op (l ++ nil) = G op l. + +(* Ensure that conversion of terms with evars is allowed once a keyed candidate unifier is found *) +rewrite -> list_foo. +reflexivity. +Qed. + +(* Basically like list_foo, but now uses the op projection for everything *) +Lemma test2 A (l : list A) : G op (op l nil) = G op l. +Proof. +rewrite ->list_foo. +reflexivity. +Qed. + + Require Import Bool. + Set Keyed Unification. + + Lemma test b : b && true = b. + Fail rewrite andb_true_l. + Admitted.
\ No newline at end of file diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v index 54cfa658..45c1a5e5 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-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \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 d6bbfe29..878875bd 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -242,7 +242,7 @@ Fail Check (Prop : Set). Fail Check (Set : Set). Check (Set : Type). Check (Prop : Type). -Definition setType := $(let t := type of Set in exact t)$. +Definition setType := ltac:(let t := type of Set in exact t). Definition foo (A : Prop) := A. @@ -303,7 +303,7 @@ Set Printing Universes. Axiom admit : forall A, A. Record R := {O : Type}. -Definition RL (x : R@{i}) : $(let u := constr:(Type@{i}:Type@{j}) in exact (R@{j}) )$ := {|O := @O x|}. +Definition RL (x : R@{i}) : ltac:(let u := constr:(Type@{i}:Type@{j}) in exact (R@{j}) ) := {|O := @O x|}. Definition RLRL : forall x : R, RL x = RL (RL x) := fun x => eq_refl. Definition RLRL' : forall x : R, RL x = RL (RL x). intros. apply eq_refl. diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 125615c5..281d707c 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -194,4 +194,17 @@ 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. Recursive Extraction term term'. -(*Unset Printing Primitive Projection Parameters.*)
\ No newline at end of file +(*Unset Printing Primitive Projection Parameters.*) + +(* Primitive projections in the presence of let-ins (was not failing in beta3)*) + +Set Primitive Projections. +Record s (x:nat) (y:=S x) := {c:=x; d:x=c}. +Lemma f : 0=1. +Proof. +Fail apply d. +(* +split. +reflexivity. +Qed. +*) diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v index c83f45e2..adaa05ad 100644 --- a/test-suite/success/proof_using.v +++ b/test-suite/success/proof_using.v @@ -178,6 +178,7 @@ End Let. Check (test_let 3). +(* Disabled Section Clear. Variable a: nat. @@ -192,6 +193,6 @@ trivial. Qed. End Clear. - +*) diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index 1e667884..352abb2a 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -62,7 +62,7 @@ Abort. Goal (forall n : nat, n = 0 -> Prop) -> Prop. intro P. refine (P _ _). -2:reflexivity. +reflexivity. Abort. (* Submitted by Jacek Chrzaszcz (bug #1102) *) diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index 2954e255..d595cbc2 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-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/unshelve.v b/test-suite/success/unshelve.v new file mode 100644 index 00000000..672222bd --- /dev/null +++ b/test-suite/success/unshelve.v @@ -0,0 +1,11 @@ +Axiom F : forall (b : bool), b = true -> + forall (i : unit), i = i -> True. + +Goal True. +Proof. +unshelve (refine (F _ _ _ _)). ++ exact true. ++ exact tt. ++ exact (@eq_refl bool true). ++ exact (@eq_refl unit tt). +Qed. diff --git a/test-suite/kernel/vm-univ.v b/test-suite/success/vm_univ_poly.v index 1bdba3c6..58fa3974 100644 --- a/test-suite/kernel/vm-univ.v +++ b/test-suite/success/vm_univ_poly.v @@ -37,32 +37,30 @@ Definition _4 : sumbool_copy x = x := @eq_refl _ x <: sumbool_copy x = x. (* Polymorphic Inductive Types *) -Polymorphic Inductive poption (T : Type@{i}) : Type@{i} := +Polymorphic Inductive poption@{i} (T : Type@{i}) : Type@{i} := | PSome : T -> poption@{i} T | PNone : poption@{i} T. -Polymorphic Definition poption_default {T : Type@{i}} (p : poption@{i} T) (x : T) : T := +Polymorphic Definition poption_default@{i} {T : Type@{i}} (p : poption@{i} T) (x : T) : T := match p with | @PSome _ y => y | @PNone _ => x end. -Polymorphic Inductive plist (T : Type@{i}) : Type@{i} := +Polymorphic Inductive plist@{i} (T : Type@{i}) : Type@{i} := | pnil | pcons : T -> plist@{i} T -> plist@{i} T. Arguments pnil {_}. Arguments pcons {_} _ _. -Section pmap. - Context {T : Type@{i}} {U : Type@{j}} (f : T -> U). - - Polymorphic Fixpoint pmap (ls : plist@{i} T) : plist@{j} U := +Polymorphic Definition pmap@{i j} + {T : Type@{i}} {U : Type@{j}} (f : T -> U) := + fix pmap (ls : plist@{i} T) : plist@{j} U := match ls with | @pnil _ => @pnil _ | @pcons _ l ls => @pcons@{j} U (f l) (pmap@{i j} ls) end. -End pmap. Universe Ubool. Inductive tbool : Type@{Ubool} := ttrue | tfalse. @@ -75,59 +73,57 @@ Eval vm_compute in pmap (fun x => match x with end) (pcons pnil (pcons (pcons false pnil) pnil)). Eval vm_compute in pmap (fun x => x -> Type) (pcons tbool (pcons (plist tbool) pnil)). -Polymorphic Inductive Tree (T : Type@{i}) : Type@{i} := +Polymorphic Inductive Tree@{i} (T : Type@{i}) : Type@{i} := | Empty | Branch : plist@{i} (Tree@{i} T) -> Tree@{i} T. -Section pfold. - Context {T : Type@{i}} {U : Type@{u}} (f : T -> U -> U). - - Polymorphic Fixpoint pfold (acc : U) (ls : plist@{i} T) : U := +Polymorphic Definition pfold@{i u} + {T : Type@{i}} {U : Type@{u}} (f : T -> U -> U) := + fix pfold (acc : U) (ls : plist@{i} T) : U := match ls with | pnil => acc | pcons a b => pfold (f a acc) b end. -End pfold. -Polymorphic Inductive nat : Type@{i} := +Polymorphic Inductive nat@{i} : Type@{i} := | O | S : nat -> nat. -Fixpoint nat_max (a b : nat) : nat := +Polymorphic Fixpoint nat_max@{i} (a b : nat@{i}) : nat@{i} := match a , b with | O , b => b | a , O => a | S a , S b => S (nat_max a b) end. -Polymorphic Fixpoint height {T : Type@{i}} (t : Tree@{i} T) : nat := - match t with +Polymorphic Fixpoint height@{i} {T : Type@{i}} (t : Tree@{i} T) : nat@{i} := + match t return nat@{i} with | Empty _ => O - | Branch _ ls => S (pfold nat_max O (pmap height ls)) + | Branch _ ls => S@{i} (pfold@{i i} nat_max O (pmap height ls)) end. -Polymorphic Fixpoint repeat {T : Type@{i}} (n : nat) (v : T) : plist@{i} T := - match n with +Polymorphic Fixpoint repeat@{i} {T : Type@{i}} (n : nat@{i}) (v : T) : plist@{i} T := + match n return plist@{i} T with | O => pnil - | S n => pcons v (repeat n v) + | S n => pcons@{i} v (repeat n v) end. -Polymorphic Fixpoint big_tree (n : nat) : Tree@{i} nat := +Polymorphic Fixpoint big_tree@{i} (n : nat@{i}) : Tree@{i} nat@{i} := match n with - | O => @Empty nat - | S n' => Branch _ (repeat n' (big_tree n')) + | O => @Empty nat@{i} + | S n' => Branch@{i} nat@{i} (repeat@{i} n' (big_tree@{i} n')) end. Eval compute in height (big_tree (S (S (S O)))). Let big := S (S (S (S (S O)))). -Polymorphic Definition really_big := (S@{i} (S (S (S (S (S (S (S (S (S O)))))))))). +Polymorphic Definition really_big@{i} := (S@{i} (S (S (S (S (S (S (S (S (S O)))))))))). Time Definition _5 : height (@Empty nat) = O := @eq_refl nat O <: height (@Empty nat) = O. Time Definition _6 : height@{Set} (@Branch nat pnil) = S O := - @eq_refl nat@{Set} (S@{Set} O@{Set}) <: height@{Set} (@Branch nat pnil) = S O. + @eq_refl nat@{Set} (S@{Set} O@{Set}) <: @eq nat@{Set} (height@{Set} (@Branch@{Set} nat@{Set} (@pnil@{Set} (Tree@{Set} nat@{Set})))) (S@{Set} O@{Set}). Time Definition _7 : height (big_tree big) = big := @eq_refl nat big <: height (big_tree big) = big. diff --git a/test-suite/success/vm_univ_poly_match.v b/test-suite/success/vm_univ_poly_match.v new file mode 100644 index 00000000..abe6d0fe --- /dev/null +++ b/test-suite/success/vm_univ_poly_match.v @@ -0,0 +1,28 @@ +Set Dump Bytecode. +Set Printing Universes. +Set Printing All. + +Polymorphic Class Applicative@{d c} (T : Type@{d} -> Type@{c}) := +{ pure : forall {A : Type@{d}}, A -> T A + ; ap : forall {A B : Type@{d}}, T (A -> B) -> T A -> T B +}. + +Universes Uo Ua. + +Eval compute in @pure@{Uo Ua}. + +Global Instance Applicative_option : Applicative@{Uo Ua} option := +{| pure := @Some + ; ap := fun _ _ f x => + match f , x with + | Some f , Some x => Some (f x) + | _ , _ => None + end +|}. + +Definition foo := ap (ap (pure plus) (pure 1)) (pure 1). + +Print foo. + + +Eval vm_compute in foo. diff --git a/test-suite/typeclasses/NewSetoid.v b/test-suite/typeclasses/NewSetoid.v index 6f37de65..49f20a23 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-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |