diff options
Diffstat (limited to 'test-suite/failure')
-rw-r--r-- | test-suite/failure/Tauto.v | 10 | ||||
-rw-r--r-- | test-suite/failure/circular_subtyping.v | 2 | ||||
-rw-r--r-- | test-suite/failure/clash_cons.v | 10 | ||||
-rw-r--r-- | test-suite/failure/cofixpoint.v | 2 | ||||
-rw-r--r-- | test-suite/failure/fixpoint1.v | 10 | ||||
-rw-r--r-- | test-suite/failure/fixpointeta.v | 70 | ||||
-rw-r--r-- | test-suite/failure/guard-cofix.v | 2 | ||||
-rw-r--r-- | test-suite/failure/guard.v | 10 | ||||
-rw-r--r-- | test-suite/failure/illtype1.v | 10 | ||||
-rw-r--r-- | test-suite/failure/int31.v | 2 | ||||
-rw-r--r-- | test-suite/failure/positivity.v | 10 | ||||
-rw-r--r-- | test-suite/failure/proofirrelevance.v | 5 | ||||
-rw-r--r-- | test-suite/failure/redef.v | 10 | ||||
-rw-r--r-- | test-suite/failure/search.v | 10 | ||||
-rw-r--r-- | test-suite/failure/sortelim.v | 2 |
15 files changed, 125 insertions, 40 deletions
diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v index d91d159d..81d5b635 100644 --- a/test-suite/failure/Tauto.v +++ b/test-suite/failure/Tauto.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (**** Tactics Tauto and Intuition ****) diff --git a/test-suite/failure/circular_subtyping.v b/test-suite/failure/circular_subtyping.v index ceccd460..9eb7e3bc 100644 --- a/test-suite/failure/circular_subtyping.v +++ b/test-suite/failure/circular_subtyping.v @@ -7,4 +7,4 @@ Module NN <: T. Module M:=N. End NN. Fail Module P <: T with Module M:=NN := NN. Module F (X:S) (Y:T with Module M:=X). End F. -Fail Module G := F N N.
\ No newline at end of file +Fail Module G := F N N. diff --git a/test-suite/failure/clash_cons.v b/test-suite/failure/clash_cons.v index b3fbff68..89299110 100644 --- a/test-suite/failure/clash_cons.v +++ b/test-suite/failure/clash_cons.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Teste la verification d'unicite des noms de constr *) diff --git a/test-suite/failure/cofixpoint.v b/test-suite/failure/cofixpoint.v index cb39893f..d193dc48 100644 --- a/test-suite/failure/cofixpoint.v +++ b/test-suite/failure/cofixpoint.v @@ -12,4 +12,4 @@ Fail CoFixpoint loop : CoFalse := (cofix f := I with g := loop for g). Fail CoFixpoint loop : CoFalse := - (cofix f := loop with g := I for f).
\ No newline at end of file + (cofix f := loop with g := I for f). diff --git a/test-suite/failure/fixpoint1.v b/test-suite/failure/fixpoint1.v index c2b521c2..eb3d9452 100644 --- a/test-suite/failure/fixpoint1.v +++ b/test-suite/failure/fixpoint1.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Fail Fixpoint PreParadox (u : unit) : False := PreParadox u. (*Definition Paradox := PreParadox tt.*) diff --git a/test-suite/failure/fixpointeta.v b/test-suite/failure/fixpointeta.v new file mode 100644 index 00000000..9af71932 --- /dev/null +++ b/test-suite/failure/fixpointeta.v @@ -0,0 +1,70 @@ + +Set Primitive Projections. + +Record R := C { p : nat }. +(* R is defined +p is defined *) + +Unset Primitive Projections. +Record R' := C' { p' : nat }. + + + +Fail Definition f := fix f (x : R) : nat := p x. +(** Not allowed to make fixpoint defs on (non-recursive) records + having eta *) + +Fail Definition f := fix f (x : R') : nat := p' x. +(** Even without eta (R' is not primitive here), as long as they're + found to be BiFinite (non-recursive), we disallow it *) + +(* + +(* Subject reduction failure example, if we allowed fixpoints *) + +Set Primitive Projections. + +Record R := C { p : nat }. + +Definition f := fix f (x : R) : nat := p x. + +(* eta rule for R *) +Definition Rtr (P : R -> Type) x (v : P (C (p x))) : P x + := v. + +Definition goal := forall x, f x = p x. + +(* when we compute the Rtr away typechecking will fail *) +Definition thing : goal := fun x => +(Rtr (fun x => f x = p x) x (eq_refl _)). + +Definition thing' := Eval compute in thing. + +Fail Check (thing = thing'). +(* +The command has indeed failed with message: +The term "thing'" has type "forall x : R, (let (p) := x in p) = (let (p) := x in p)" +while it is expected to have type "goal" (cannot unify "(let (p) := x in p) = (let (p) := x in p)" +and "f x = p x"). +*) + +Definition thing_refl := eq_refl thing. + +Fail Definition thing_refl' := Eval compute in thing_refl. +(* +The command has indeed failed with message: +Illegal application: +The term "@eq_refl" of type "forall (A : Type) (x : A), x = x" +cannot be applied to the terms + "forall x : R, (fix f (x0 : R) : nat := let (p) := x0 in p) x = (let (p) := x in p)" : "Prop" + "fun x : R => eq_refl" : "forall x : R, (let (p) := x in p) = (let (p) := x in p)" +The 2nd term has type "forall x : R, (let (p) := x in p) = (let (p) := x in p)" +which should be coercible to + "forall x : R, (fix f (x0 : R) : nat := let (p) := x0 in p) x = (let (p) := x in p)". + *) + +Definition more_refls : thing_refl = thing_refl. +Proof. + compute. reflexivity. +Fail Defined. Abort. + *) diff --git a/test-suite/failure/guard-cofix.v b/test-suite/failure/guard-cofix.v index eda4a186..3ae87705 100644 --- a/test-suite/failure/guard-cofix.v +++ b/test-suite/failure/guard-cofix.v @@ -40,4 +40,4 @@ Fail CoFixpoint loop' : CoFalse := Omega match eq_sym H in _ = T return T with eq_refl => loop' end end. -Fail Definition ff' : False := match loop' with CF _ t => t end.
\ No newline at end of file +Fail Definition ff' : False := match loop' with CF _ t => t end. diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v index 8db27858..2a5ad778 100644 --- a/test-suite/failure/guard.v +++ b/test-suite/failure/guard.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Fixpoint F (n:nat) : False := F (match F n with end). diff --git a/test-suite/failure/illtype1.v b/test-suite/failure/illtype1.v index 8ed3af1c..ec43ea5f 100644 --- a/test-suite/failure/illtype1.v +++ b/test-suite/failure/illtype1.v @@ -1,8 +1,10 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Fail Check (S S). diff --git a/test-suite/failure/int31.v b/test-suite/failure/int31.v index b1d11224..ed4c9f9c 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 8089de2b..2798dcf9 100644 --- a/test-suite/failure/positivity.v +++ b/test-suite/failure/positivity.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Negative occurrence *) diff --git a/test-suite/failure/proofirrelevance.v b/test-suite/failure/proofirrelevance.v index b62f9b68..bb9579d4 100644 --- a/test-suite/failure/proofirrelevance.v +++ b/test-suite/failure/proofirrelevance.v @@ -1,6 +1,5 @@ -(* This was working in version 8.1beta (bug in the Sort-polymorphism - of inductive types), but this is inconsistent with classical logic - in Prop *) +(* This was working in version 8.1beta (bug in template polymorphism), + but this is inconsistent with classical logic in Prop *) Inductive bool_in_prop : Type := hide : bool -> bool_in_prop with bool : Type := true : bool | false : bool. diff --git a/test-suite/failure/redef.v b/test-suite/failure/redef.v index c8dc6303..981d1438 100644 --- a/test-suite/failure/redef.v +++ b/test-suite/failure/redef.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Definition toto := Set. Fail Definition toto := Set. diff --git a/test-suite/failure/search.v b/test-suite/failure/search.v index 648ab082..058c427c 100644 --- a/test-suite/failure/search.v +++ b/test-suite/failure/search.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Fail SearchPattern (_ = _) outside n_existe_pas. diff --git a/test-suite/failure/sortelim.v b/test-suite/failure/sortelim.v index 2b3cf106..3d2eef6a 100644 --- a/test-suite/failure/sortelim.v +++ b/test-suite/failure/sortelim.v @@ -146,4 +146,4 @@ Qed. Print Assumptions pandora. -*)
\ No newline at end of file +*) |