diff options
Diffstat (limited to 'test-suite')
73 files changed, 752 insertions, 255 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 16a56f4408..8239600b1d 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -1,10 +1,12 @@ -####################################################################### -# v # The Coq Proof Assistant / The Coq Development Team # -# <O___,, # INRIA-Rocquencourt & CNRS-Universite Paris Diderot # -# \VV/ ############################################################# -# // # This file is distributed under the terms of the # -# # GNU Lesser General Public License Version 2.1 # -####################################################################### +########################################################################## +## # 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 ## +## # (see LICENSE file for the text of the license) ## +########################################################################## # This is a standalone Makefile to run the test-suite. It can be used # outside of the Coq source tree (if BIN is overridden). diff --git a/test-suite/bugs/closed/2850.v b/test-suite/bugs/closed/2850.v deleted file mode 100644 index 64a93aeb00..0000000000 --- a/test-suite/bugs/closed/2850.v +++ /dev/null @@ -1,2 +0,0 @@ -Definition id {A} (x : A) := x. -Fail Compute id. diff --git a/test-suite/bugs/closed/3481.v b/test-suite/bugs/closed/3481.v index 89d476dcb1..38f03b166b 100644 --- a/test-suite/bugs/closed/3481.v +++ b/test-suite/bugs/closed/3481.v @@ -3,7 +3,7 @@ Set Implicit Arguments. Require Import Logic. Module NonPrim. -Local Set Record Elimination Schemes. +Local Set Nonrecursive Elimination Schemes. Record prodwithlet (A B : Type) : Type := pair' { fst : A; fst' := fst; snd : B }. @@ -21,7 +21,7 @@ End NonPrim. Global Set Universe Polymorphism. Global Set Asymmetric Patterns. -Local Set Record Elimination Schemes. +Local Set Nonrecursive Elimination Schemes. Local Set Primitive Projections. Record prod (A B : Type) : Type := diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v index 5adc48215e..1f0f3b0da9 100644 --- a/test-suite/bugs/closed/3513.v +++ b/test-suite/bugs/closed/3513.v @@ -69,26 +69,6 @@ Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred) refine (P _ _) end; unfold Basics.flip. Focus 2. - Set Typeclasses Debug. - Set Typeclasses Legacy Resolution. - apply reflexivity. - (* Debug: 1.1: apply @IsPointed_catOP on -(IsPointed (exists x0 : Actions, (catOP ?Goal O2 : OPred) x0)) -Debug: 1.1.1.1: apply OPred_inhabited on (IsPointed (exists x0 : Actions, ?Goal x0)) -Debug: 1.1.2.1: apply OPred_inhabited on (IsPointed (exists x : Actions, O2 x)) -Debug: 2.1: apply @Equivalence_Reflexive on (Reflexive lentails) -Debug: 2.1.1: no match for (Equivalence lentails) , 5 possibilities -Debug: Backtracking after apply @Equivalence_Reflexive -Debug: 2.2: apply @PreOrder_Reflexive on (Reflexive lentails) -Debug: 2.2.1.1: apply @lentailsPre on (PreOrder lentails) -Debug: 2.2.1.1.1.1: apply ILFun_ILogic on (ILogic OPred) -*) - Undo. Unset Typeclasses Legacy Resolution. - Test Typeclasses Unique Solutions. - Test Typeclasses Unique Instances. - Show Existentials. - Set Typeclasses Debug Verbosity 2. - Set Printing All. (* As in 8.5, allow a shelved subgoal to remain *) apply reflexivity. diff --git a/test-suite/bugs/closed/3520.v b/test-suite/bugs/closed/3520.v index c981207e6b..ea122e521f 100644 --- a/test-suite/bugs/closed/3520.v +++ b/test-suite/bugs/closed/3520.v @@ -3,7 +3,7 @@ Set Primitive Projections. Record foo (A : Type) := { bar : Type ; baz := Set; bad : baz = bar }. -Set Record Elimination Schemes. +Set Nonrecursive Elimination Schemes. Record notprim : Prop := { irrel : True; relevant : nat }. diff --git a/test-suite/bugs/closed/3662.v b/test-suite/bugs/closed/3662.v index bd53389b4f..b8754bce98 100644 --- a/test-suite/bugs/closed/3662.v +++ b/test-suite/bugs/closed/3662.v @@ -1,6 +1,6 @@ Set Primitive Projections. Set Implicit Arguments. -Set Record Elimination Schemes. +Set Nonrecursive Elimination Schemes. Record prod A B := pair { fst : A ; snd : B }. Definition f : Set -> Type := fun x => x. diff --git a/test-suite/bugs/closed/4785.v b/test-suite/bugs/closed/4785.v index c3c97d3f59..0d347b262d 100644 --- a/test-suite/bugs/closed/4785.v +++ b/test-suite/bugs/closed/4785.v @@ -1,5 +1,4 @@ Require Coq.Lists.List Coq.Vectors.Vector. -Require Coq.Compat.Coq85. Module A. Import Coq.Lists.List Coq.Vectors.Vector. @@ -21,12 +20,10 @@ Delimit Scope mylist_scope with mylist. Bind Scope mylist_scope with mylist. Arguments mynil {_}, _. Arguments mycons {_} _ _. -Notation " [] " := mynil (compat "8.5") : mylist_scope. Notation " [ ] " := mynil (format "[ ]") : mylist_scope. Notation " [ x ] " := (mycons x nil) : mylist_scope. Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope. -Import Coq.Compat.Coq85. Locate Module VectorNotations. Import VectorDef.VectorNotations. @@ -35,11 +32,3 @@ Check []%mylist : mylist _. Check [ ]%mylist : mylist _. Check [ ]%list : list _. End A. - -Module B. -Import Coq.Compat.Coq85. - -Goal True. - idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *) -Abort. -End B. diff --git a/test-suite/bugs/closed/4785_compat_85.v b/test-suite/bugs/closed/4785_compat_85.v deleted file mode 100644 index bbb34f465c..0000000000 --- a/test-suite/bugs/closed/4785_compat_85.v +++ /dev/null @@ -1,46 +0,0 @@ -(* -*- coq-prog-args: ("-compat" "8.5") -*- *) -Require Coq.Lists.List Coq.Vectors.Vector. -Require Coq.Compat.Coq85. - -Module A. -Import Coq.Lists.List Coq.Vectors.Vector. -Import ListNotations. -Check [ ]%list : list _. -Import VectorNotations ListNotations. -Delimit Scope vector_scope with vector. -Check [ ]%vector : Vector.t _ _. -Check []%vector : Vector.t _ _. -Check [ ]%list : list _. -Fail Check []%list : list _. - -Goal True. - idtac; [ ]. (* Note that vector notations break the [ | .. | ] syntax of Ltac *) -Abort. - -Inductive mylist A := mynil | mycons (x : A) (xs : mylist A). -Delimit Scope mylist_scope with mylist. -Bind Scope mylist_scope with mylist. -Arguments mynil {_}, _. -Arguments mycons {_} _ _. -Notation " [] " := mynil (compat "8.5") : mylist_scope. -Notation " [ ] " := mynil (format "[ ]") : mylist_scope. -Notation " [ x ] " := (mycons x nil) : mylist_scope. -Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope. - -Import Coq.Compat.Coq85. -Locate Module VectorNotations. -Import VectorDef.VectorNotations. - -Check []%vector : Vector.t _ _. -Check []%mylist : mylist _. -Check [ ]%mylist : mylist _. -Check [ ]%list : list _. -End A. - -Module B. -Import Coq.Compat.Coq85. - -Goal True. - idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *) -Abort. -End B. diff --git a/test-suite/bugs/closed/4798.v b/test-suite/bugs/closed/4798.v index dbc3d46fce..6f2bcb9685 100644 --- a/test-suite/bugs/closed/4798.v +++ b/test-suite/bugs/closed/4798.v @@ -1,3 +1,3 @@ Check match 2 with 0 => 0 | S n => n end. -Notation "|" := 1 (compat "8.4"). +Notation "|" := 1 (compat "8.6"). Check match 2 with 0 => 0 | S n => n end. (* fails *) diff --git a/test-suite/bugs/closed/4873.v b/test-suite/bugs/closed/4873.v index 3be36d8475..39299883ad 100644 --- a/test-suite/bugs/closed/4873.v +++ b/test-suite/bugs/closed/4873.v @@ -1,6 +1,5 @@ Require Import Coq.Classes.Morphisms. Require Import Relation_Definitions. -Require Import Coq.Compat.Coq85. Fixpoint tuple' T n : Type := match n with diff --git a/test-suite/bugs/closed/5532.v b/test-suite/bugs/closed/5532.v new file mode 100644 index 0000000000..ee5446e548 --- /dev/null +++ b/test-suite/bugs/closed/5532.v @@ -0,0 +1,15 @@ +(* A wish granted by the new support for patterns in notations *) + +Local Notation mkmatch0 e p + := match e with + | p => true + | _ => false + end. +Local Notation "'mkmatch' [[ e ]] [[ p ]]" + := match e with + | p => true + | _ => false + end + (at level 0, p pattern). +Check mkmatch0 _ ((0, 0)%core). +Check mkmatch [[ _ ]] [[ ((0, 0)%core) ]]. diff --git a/test-suite/bugs/closed/6529.v b/test-suite/bugs/closed/6529.v new file mode 100644 index 0000000000..8d90819998 --- /dev/null +++ b/test-suite/bugs/closed/6529.v @@ -0,0 +1,16 @@ +Require Import Vector Program. + +Program Definition append_nil_def := + forall A n (ls: t A n), append ls (nil A) = ls. (* Works *) + +Lemma append_nil : append_nil_def. (* Works *) +Proof. +Admitted. + +Program Lemma append_nil' : + forall A n (ls: t A n), append ls (nil A) = ls. +Abort. + +Fail Program Lemma append_nil'' : + forall A B n (ls: t A n), append ls (nil A) = ls. +(* Error: Anomaly "Evar ?X25 was not declared." Please report at http://coq.inria.fr/bugs/. *) diff --git a/test-suite/bugs/closed/6677.v b/test-suite/bugs/closed/6677.v new file mode 100644 index 0000000000..99e47bb87c --- /dev/null +++ b/test-suite/bugs/closed/6677.v @@ -0,0 +1,5 @@ +Set Universe Polymorphism. + +Definition T@{i} := Type@{i}. +Fail Definition U@{i} := (T@{i} <: Type@{i}). +Fail Definition eqU@{i j} : @eq T@{j} U@{i} T@{i} := eq_refl. diff --git a/test-suite/bugs/closed/6774.v b/test-suite/bugs/closed/6774.v new file mode 100644 index 0000000000..9625af91f5 --- /dev/null +++ b/test-suite/bugs/closed/6774.v @@ -0,0 +1,7 @@ +(* Was an anomaly with ill-typed template polymorphism *) +Definition huh (b:bool) := if b then Set else Prop. +Definition lol b: huh b := + if b return huh b then nat else True. +Goal (lol true) * unit. +Fail generalize true. (* should fail with error, not anomaly *) +Abort. diff --git a/test-suite/bugs/closed/6878.v b/test-suite/bugs/closed/6878.v new file mode 100644 index 0000000000..70f1b3127a --- /dev/null +++ b/test-suite/bugs/closed/6878.v @@ -0,0 +1,8 @@ + +Set Universe Polymorphism. +Module Type T. + Axiom foo : Prop. +End T. + +(** Used to anomaly *) +Fail Module M : T with Definition foo := Type. diff --git a/test-suite/bugs/closed/HoTT_coq_077.v b/test-suite/bugs/closed/HoTT_coq_077.v index 017780c1f3..f69c71a026 100644 --- a/test-suite/bugs/closed/HoTT_coq_077.v +++ b/test-suite/bugs/closed/HoTT_coq_077.v @@ -3,7 +3,7 @@ Set Implicit Arguments. Require Import Logic. Set Asymmetric Patterns. -Set Record Elimination Schemes. +Set Nonrecursive Elimination Schemes. Set Primitive Projections. Record prod (A B : Type) : Type := diff --git a/test-suite/bugs/closed/HoTT_coq_104.v b/test-suite/bugs/closed/HoTT_coq_104.v index 5bb7fa8c12..a6ff78d127 100644 --- a/test-suite/bugs/closed/HoTT_coq_104.v +++ b/test-suite/bugs/closed/HoTT_coq_104.v @@ -4,7 +4,7 @@ Require Import Logic. Global Set Universe Polymorphism. Global Set Asymmetric Patterns. -Local Set Record Elimination Schemes. +Local Set Nonrecursive Elimination Schemes. Local Set Primitive Projections. Record prod (A B : Type) : Type := diff --git a/test-suite/bugs/opened/3926.v b/test-suite/bugs/opened/3926.v deleted file mode 100644 index cfad763572..0000000000 --- a/test-suite/bugs/opened/3926.v +++ /dev/null @@ -1,30 +0,0 @@ -Notation compose := (fun g f x => g (f x)). -Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope. -Open Scope function_scope. -Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. -Arguments idpath {A a} , [A] a. -Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with idpath => idpath end. -Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A }. -Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope. -Local Open Scope equiv_scope. -Axiom eisretr : forall {A B} (f : A -> B) `{IsEquiv A B f} x, f (f^-1 x) = x. -Generalizable Variables A B C f g. -Global Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g} : IsEquiv (compose g f) | 1000 - := Build_IsEquiv A C (compose g f) (compose f^-1 g^-1). -Definition isequiv_homotopic {A B} (f : A -> B) {g : A -> B} `{IsEquiv A B f} (h : forall x, f x = g x) : IsEquiv g - := Build_IsEquiv _ _ g (f ^-1). -Global Instance isequiv_inverse {A B} (f : A -> B) `{IsEquiv A B f} : IsEquiv f^-1 | 10000 - := Build_IsEquiv B A f^-1 f. -Definition cancelR_isequiv {A B C} (f : A -> B) {g : B -> C} - `{IsEquiv A B f} `{IsEquiv A C (g o f)} - : IsEquiv g. -Proof. - Unset Typeclasses Modulo Eta. - exact (isequiv_homotopic (compose (compose g f) f^-1) - (fun b => ap g (eisretr f b))) || fail "too early". - Undo. - Set Typeclasses Modulo Eta. - Set Typeclasses Dependency Order. - Set Typeclasses Debug. - Fail exact (isequiv_homotopic (compose (compose g f) f^-1) - (fun b => ap g (eisretr f b))). diff --git a/test-suite/bugs/opened/6602.v b/test-suite/bugs/opened/6602.v new file mode 100644 index 0000000000..3690adf90a --- /dev/null +++ b/test-suite/bugs/opened/6602.v @@ -0,0 +1,17 @@ +Require Import Omega. + +Lemma test_nat: + forall n, (5 + pred n <= 5 + n). +Proof. + intros. + zify. + omega. +Qed. + +Lemma test_N: + forall n, (5 + N.pred n <= 5 + n)%N. +Proof. + intros. + zify. + omega. +Qed. diff --git a/test-suite/coq-makefile/emptyprefix/_CoqProject b/test-suite/coq-makefile/emptyprefix/_CoqProject new file mode 100644 index 0000000000..5678a8edbb --- /dev/null +++ b/test-suite/coq-makefile/emptyprefix/_CoqProject @@ -0,0 +1,11 @@ +-R theories "" +-R src "" +-I src +-arg "-w default" + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/emptyprefix/_CoqProject.sub b/test-suite/coq-makefile/emptyprefix/_CoqProject.sub new file mode 100644 index 0000000000..90ac541e04 --- /dev/null +++ b/test-suite/coq-makefile/emptyprefix/_CoqProject.sub @@ -0,0 +1,3 @@ +-R ../theories "" +-I ../src +testsub.v diff --git a/test-suite/coq-makefile/emptyprefix/run.sh b/test-suite/coq-makefile/emptyprefix/run.sh new file mode 100755 index 0000000000..a10e63b42e --- /dev/null +++ b/test-suite/coq-makefile/emptyprefix/run.sh @@ -0,0 +1,17 @@ +#!/usr/bin/env bash + +set -e + +. ../template/init.sh + +mv theories/sub theories2 + +coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf +make + +cp ../_CoqProject.sub theories2/_CoqProject +cd theories2 +coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf +make diff --git a/test-suite/coq-makefile/quick2vo/_CoqProject b/test-suite/coq-makefile/quick2vo/_CoqProject new file mode 100644 index 0000000000..69f47302e1 --- /dev/null +++ b/test-suite/coq-makefile/quick2vo/_CoqProject @@ -0,0 +1,10 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/quick2vo/run.sh b/test-suite/coq-makefile/quick2vo/run.sh new file mode 100755 index 0000000000..9e681223b4 --- /dev/null +++ b/test-suite/coq-makefile/quick2vo/run.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash +a=`uname` + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +# vio2vo is broken on Windows (#6720) +if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then + make quick2vo J=2 + test -f theories/test.vo + make validate +fi diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index 2439d3f378..aa6b0a9a43 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -38,9 +38,29 @@ make print-pretty-timed-diff TIMING_SORT_BY=diff || exit $? INFINITY="∞" INFINITY_REPLACEMENT="+.%" # assume that if the before time is zero, we expected the time to increase +TO_SED_IN_BOTH=( + -e s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" # Whether or not something shows up as ∞ depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent + -e s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" # Whether or not something shows up as N/A depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent + -e s'/ *$//g' # the number of trailing spaces depends on how many digits percentages end up being; since this varies across runs, we remove trailing spaces + -e s'/[0-9]*\.[0-9]*//g' # the precise timing numbers vary, so we strip them out + -e s'/^-*$/------/g' # When none of the numbers get over 100 (or 1000, in per-file), the width of the table is different, so we normalize the number of dashes for table separators +) + +TO_SED_IN_PER_FILE=( + -e s'/[0-9]//g' # unclear whether this is actually needed above and beyond s'/[0-9]*\.[0-9]*//g'; it's been here from the start + -e s'/ */ /g' # unclear whether this is actually needed for per-file timing; it's been here from the start + -e s'/\(Total.*\)-\(.*\)-/\1+\2+/g' # Overall time in the per-file timing diff should be around 0; if it comes out negative, we remove the sign +) + +TO_SED_IN_PER_LINE=( + -e s'/0//g' # unclear whether this is actually needed above and beyond s'/[0-9]*\.[0-9]*//g'; it's been here from the start + -e s'/ */ /g' # Sometimes 0 will show up as 0m00.s, sometimes it'll end up being more like 0m00.001s; we must strip out the spaces that result from left-aligning numbers of different widths based on how many digits Coq's [-time] gives + -e s'/+/-/g' # some code lines don't really change, but this can show up as either -0m00.01s or +0m00.01s, so we need to normalize the signs + ) + for ext in "" .desired; do for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do - cat ${file}${ext} | grep -v 'warning: undefined variable' | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s'/[0-9]//g' | sed s'/ *$//g' | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/^-*$/------/g' | sed s'/ */ /g' | sed s'/\(Total.*\)-\(.*\)-/\1+\2+/g' > ${file}${ext}.processed + cat ${file}${ext} | grep -v 'warning: undefined variable' | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" > ${file}${ext}.processed done done for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do @@ -74,7 +94,7 @@ echo for ext in "" .desired; do for file in A.v.timing.diff; do - cat ${file}${ext} | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/[0-9]*\.[0-9]*//g' | sed s'/0//g' | sed s'/ */ /g' | sed s'/ *$//g' | sed s'/+/-/g' | sort > ${file}${ext}.processed + cat ${file}${ext} | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_LINE[@]}" | sort > ${file}${ext}.processed done done for file in A.v.timing.diff; do diff --git a/test-suite/coq-makefile/vio2vo/_CoqProject b/test-suite/coq-makefile/vio2vo/_CoqProject new file mode 100644 index 0000000000..69f47302e1 --- /dev/null +++ b/test-suite/coq-makefile/vio2vo/_CoqProject @@ -0,0 +1,10 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/vio2vo/run.sh b/test-suite/coq-makefile/vio2vo/run.sh new file mode 100755 index 0000000000..85656da419 --- /dev/null +++ b/test-suite/coq-makefile/vio2vo/run.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash +a=`uname` + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +make quick +# vio2vo is broken on Windows (#6720) +if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then + make vio2vo J=2 + test -f theories/test.vo + make validate +fi diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v index 19976b41bd..81d5b6358e 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-2017 *) +(* * 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/clash_cons.v b/test-suite/failure/clash_cons.v index 1761cc437d..89299110be 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-2017 *) +(* * 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/fixpoint1.v b/test-suite/failure/fixpoint1.v index 0739982442..eb3d94526c 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-2017 *) +(* * 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/guard.v b/test-suite/failure/guard.v index 312dc48bea..2a5ad7789c 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-2017 *) +(* * 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 fdd1bddd88..ec43ea5fc8 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-2017 *) +(* * 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/positivity.v b/test-suite/failure/positivity.v index b21204b9e4..2798dcf974 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-2017 *) +(* * 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/redef.v b/test-suite/failure/redef.v index c49dbd7cae..981d14387d 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-2017 *) +(* * 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 fae6cd6f3b..058c427c93 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-2017 *) +(* * 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/ideal-features/Apply.v b/test-suite/ideal-features/Apply.v index 85680e94b9..14eb1e3f96 100644 --- a/test-suite/ideal-features/Apply.v +++ b/test-suite/ideal-features/Apply.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * 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) *) (************************************************************************) (* This needs step by step unfolding *) diff --git a/test-suite/modules/SeveralWith.v b/test-suite/modules/SeveralWith.v new file mode 100644 index 0000000000..bbf72a7648 --- /dev/null +++ b/test-suite/modules/SeveralWith.v @@ -0,0 +1,12 @@ +Module Type S. +Parameter A : Type. +End S. + +Module Type ES. +Parameter A : Type. +Parameter eq : A -> A -> Type. +End ES. + +Module Make + (AX : S) + (X : ES with Definition A := AX.A with Definition eq := @eq AX.A). diff --git a/test-suite/modules/cumpoly.v b/test-suite/modules/cumpoly.v new file mode 100644 index 0000000000..654b86cb44 --- /dev/null +++ b/test-suite/modules/cumpoly.v @@ -0,0 +1,19 @@ +Set Universe Polymorphism. + +(** Check that variance subtyping is respected. The signature T is asking for + invariance, while M provide an irrelevant implementation, which is deemed + legit. + + There is currently no way to go the other way around, so it's not possible + to generate a counter-example that should fail with the wrong subtyping. +*) + +Module Type T. +Parameter t@{i|Set <= i} : Type@{i}. +Cumulative Inductive I@{i|Set <= i} : Type@{i} := C : t@{i} -> I. +End T. + +Module M : T. +Definition t@{i|Set <= i} : Type@{i} := nat. +Cumulative Inductive I@{i|Set <= i} : Type@{i} := C : t@{i} -> I. +End M. diff --git a/test-suite/output/Load.out b/test-suite/output/Load.out new file mode 100644 index 0000000000..0904d5540b --- /dev/null +++ b/test-suite/output/Load.out @@ -0,0 +1,6 @@ +f = 2 + : nat +u = I + : True +The command has indeed failed with message: +Files processed by Load cannot leave open proofs. diff --git a/test-suite/output/Load.v b/test-suite/output/Load.v new file mode 100644 index 0000000000..967507415a --- /dev/null +++ b/test-suite/output/Load.v @@ -0,0 +1,7 @@ +Load "output/load/Load_noproof.v". +Print f. + +Load "output/load/Load_proof.v". +Print u. + +Fail Load "output/load/Load_openproof.v". diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 2f0ee765db..891296b0a1 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -41,7 +41,7 @@ fun x : nat => ifn x is succ n then n else 0 -4 : Z The command has indeed failed with message: -x should not be bound in a recursive pattern of the right-hand side. +Cannot find where the recursive pattern starts. The command has indeed failed with message: in the right-hand side, y and z should appear in term position as part of a recursive pattern. diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 121a369a94..6ffe56e11f 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -17,10 +17,9 @@ fun (P : nat -> nat -> Prop) (x : nat) => exists y, P x y ∃ n p : nat, n + p = 0 : Prop let a := 0 in -∃ x y : nat, -let b := 1 in -let c := b in -let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d +∃ (x y : nat) (b := 1) (c := b) (d := 2) (z : nat), +let e := 3 in +let f := 4 in x + y = z + d : Prop ∀ n p : nat, n + p = 0 : Prop diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 531398bb0b..923caedace 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -36,8 +36,9 @@ Check fun P:nat->nat->Prop => fun x:nat => ex (P x). (* Test notations with binders *) -Notation "∃ x .. y , P":= (ex (fun x => .. (ex (fun y => P)) ..)) - (x binder, y binder, at level 200, right associativity). +Notation "∃ x .. y , P":= (ex (fun x => .. (ex (fun y => P)) ..)) + (x binder, y binder, at level 200, right associativity, + format "'[ ' ∃ x .. y ']' , P"). Check (∃ n p, n+p=0). diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 1b57252752..e6a6e0288a 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -138,3 +138,100 @@ amatch = mmatch 0 (with 0 => 1| 1 => 2 end) : unit alist = [0; 1; 2] : list nat +! '{{x, y}}, x + y = 0 + : Prop +exists x : nat, + nat -> + exists y : nat, + nat -> + exists '{{u, t}}, forall z1 : nat, z1 = 0 /\ x + y = 0 /\ u + t = 0 + : Prop +exists x : nat, + nat -> + exists y : nat, + nat -> + exists '{{z, t}}, forall z2 : nat, z2 = 0 /\ x + y = 0 /\ z + t = 0 + : Prop +exists_true '{{x, y}} (u := 0) '{{z, t}}, x + y = 0 /\ z + t = 0 + : Prop +exists_true (A : Type) (R : A -> A -> Prop) (_ : Reflexive R), +(forall x : A, R x x) + : Prop +exists_true (x : nat) (A : Type) (R : A -> A -> Prop) +(_ : Reflexive R) (y : nat), x + y = 0 -> forall z : A, R z z + : Prop +{{{{True, nat -> True}}, nat -> True}} + : Prop * Prop * Prop +{{D 1, 2}} + : nat * nat * (nat * nat * (nat * nat)) +! a b : nat # True # + : Prop * (Prop * Prop) +!!!! a b : nat # True # + : Prop * Prop * (Prop * Prop * Prop) +@@ a b : nat # a = b # b = a # + : Prop * Prop +exists_non_null x y z t : nat , x = y /\ z = t + : Prop +forall_non_null x y z t : nat , x = y /\ z = t + : Prop +{{RL 1, 2}} + : nat * (nat * nat) +{{RR 1, 2}} + : nat * nat * nat +@pair nat (prod nat nat) (S (S O)) (@pair nat nat (S O) O) + : prod nat (prod nat nat) +@pair (prod nat nat) nat (@pair nat nat O (S (S O))) (S O) + : prod (prod nat nat) nat +{{RLRR 1, 2}} + : nat * (nat * nat) * (nat * nat * nat) * (nat * (nat * nat)) * + (nat * nat * nat) +pair + (pair + (pair (pair (S (S O)) (pair (S O) O)) (pair (pair O (S (S O))) (S O))) + (pair (S O) (pair (S (S O)) O))) (pair (pair O (S O)) (S (S O))) + : prod + (prod (prod (prod nat (prod nat nat)) (prod (prod nat nat) nat)) + (prod nat (prod nat nat))) (prod (prod nat nat) nat) +fun x : nat => if x is n .+ 1 then n else 1 + : nat -> nat +{'{{x, y}} : nat * nat | x + y = 0} + : Set +exists2' {{x, y}}, x = 0 & y = 0 + : Prop +myexists2 x : nat * nat, + let '{{y, z}} := x in y > z & let '{{y, z}} := x in z > y + : Prop +fun '({{x, y}} as z) => x + y = 0 /\ z = z + : nat * nat -> Prop +myexists ({{x, y}} as z), x + y = 0 /\ z = z + : Prop +exists '({{x, y}} as z), x + y = 0 /\ z = z + : Prop +∀ '({{x, y}} as z), x + y = 0 /\ z = z + : Prop +fun '({{{{x, y}}, true}} | {{{{x, y}}, false}}) => x + y + : nat * nat * bool -> nat +myexists ({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y + : Prop +exists '({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y + : Prop +∀ '({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y + : Prop +fun p : nat => if p is S n then n else 0 + : nat -> nat +fun p : comparison => if p is Lt then 1 else 0 + : comparison -> nat +fun S : nat => [S | S + S] + : nat -> nat * (nat -> nat) +fun N : nat => [N | N + 0] + : nat -> nat * (nat -> nat) +fun S : nat => [[S | S + S]] + : nat -> nat * (nat -> nat) +{I : nat | I = I} + : Set +{'I : True | I = I} + : Prop +{'{{x, y}} : nat * nat | x + y = 0} + : Set +exists2 '{{y, z}} : nat * nat, y > z & z > y + : Prop diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index a8d6c97fbd..c98bfff413 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -253,3 +253,170 @@ Definition alist := [0;1;2]. Print alist. End B. + +(* Test contraction of "forall x, let 'pat := x in ..." into "forall 'pat, ..." *) +(* for isolated "forall" (was not working already in 8.6) *) +Notation "! x .. y , A" := (id (forall x, .. (id (forall y, A)) .. )) (at level 200, x binder). +Check ! '(x,y), x+y=0. + +(* Check that the terminator of a recursive pattern is interpreted in + the correct environment of bindings *) +Notation "'exists_mixed' x .. y , P" := (ex (fun x => forall z:nat, .. (ex (fun y => forall z:nat, z=0 /\ P)) ..)) (at level 200, x binder). +Check exists_mixed x y '(u,t), x+y=0/\u+t=0. +Check exists_mixed x y '(z,t), x+y=0/\z+t=0. + +(* Check that intermediary let-in are inserted inbetween instances of + the repeated pattern *) +Notation "'exists_true' x .. y , P" := (exists x, True /\ .. (exists y, True /\ P) ..) (at level 200, x binder). +Check exists_true '(x,y) (u:=0) '(z,t), x+y=0/\z+t=0. + +(* Check that generalized binders are correctly interpreted *) + +Module G. +Generalizable Variables A R. +Class Reflexive {A:Type} (R : A->A->Prop) := reflexivity : forall x : A, R x x. +Check exists_true `{Reflexive A R}, forall x, R x x. +Check exists_true x `{Reflexive A R} y, x+y=0 -> forall z, R z z. +End G. + +(* Allows recursive patterns for binders to be associative on the left *) +Notation "!! x .. y # A #" := (.. (A,(forall x, True)) ..,(forall y, True)) (at level 200, x binder). +Check !! a b : nat # True #. + +(* Examples where the recursive pattern refer several times to the recursive variable *) + +Notation "{{D x , .. , y }}" := ((x,x), .. ((y,y),(0,0)) ..). +Check {{D 1, 2 }}. + +Notation "! x .. y # A #" := + ((forall x, x=x), .. ((forall y, y=y), A) ..) + (at level 200, x binder). +Check ! a b : nat # True #. + +Notation "!!!! x .. y # A #" := + (((forall x, x=x),(forall x, x=0)), .. (((forall y, y=y),(forall y, y=0)), A) ..) + (at level 200, x binder). +Check !!!! a b : nat # True #. + +Notation "@@ x .. y # A # B #" := + ((forall x, .. (forall y, A) ..), (forall x, .. (forall y, B) ..)) + (at level 200, x binder). +Check @@ a b : nat # a=b # b=a #. + +Notation "'exists_non_null' x .. y , P" := + (ex (fun x => x <> 0 /\ .. (ex (fun y => y <> 0 /\ P)) ..)) + (at level 200, x binder). +Check exists_non_null x y z t , x=y/\z=t. + +Notation "'forall_non_null' x .. y , P" := + (forall x, x <> 0 -> .. (forall y, y <> 0 -> P) ..) + (at level 200, x binder). +Check forall_non_null x y z t , x=y/\z=t. + +(* Examples where the recursive pattern is in reverse order *) + +Notation "{{RL c , .. , d }}" := (pair d .. (pair c 0) ..). +Check {{RL 1 , 2}}. + +Notation "{{RR c , .. , d }}" := (pair .. (pair 0 d) .. c). +Check {{RR 1 , 2}}. + +Set Printing All. +Check {{RL 1 , 2}}. +Check {{RR 1 , 2}}. +Unset Printing All. + +Notation "{{RLRR c , .. , d }}" := (pair d .. (pair c 0) .., pair .. (pair 0 d) .. c, pair c .. (pair d 0) .., pair .. (pair 0 c) .. d). +Check {{RLRR 1 , 2}}. +Unset Printing Notations. +Check {{RLRR 1 , 2}}. +Set Printing Notations. + +(* Check insensitivity of "match" clauses to order *) + +Notation "'if' t 'is' n .+ 1 'then' p 'else' q" := + (match t with S n => p | 0 => q end) + (at level 200). +Check fun x => if x is n.+1 then n else 1. + +(* Examples with binding patterns *) + +Check {'(x,y)|x+y=0}. + +Module D. +Notation "'exists2'' x , p & q" := (ex2 (fun x => p) (fun x => q)) + (at level 200, x pattern, p at level 200, right associativity, + format "'[' 'exists2'' '/ ' x , '/ ' '[' p & '/' q ']' ']'") + : type_scope. + +Check exists2' (x,y), x=0 & y=0. +End D. + +(* Ensuring for reparsability that printer of notations does not use a + pattern where only an ident could be reparsed *) + +Module E. +Inductive myex2 {A:Type} (P Q:A -> Prop) : Prop := + myex_intro2 : forall x:A, P x -> Q x -> myex2 P Q. +Notation "'myexists2' x : A , p & q" := (myex2 (A:=A) (fun x => p) (fun x => q)) + (at level 200, x ident, A at level 200, p at level 200, right associativity, + format "'[' 'myexists2' '/ ' x : A , '/ ' '[' p & '/' q ']' ']'") + : type_scope. +Check myex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y). +End E. + +(* A canonical example of a notation with a non-recursive binder *) + +Parameter myex : forall {A}, (A -> Prop) -> Prop. +Notation "'myexists' x , p" := (myex (fun x => p)) + (at level 200, x pattern, p at level 200, right associativity). + +(* A canonical example of a notation with recursive binders *) + +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity) : type_scope. + +(* Check that printing 'pat uses an "as" when the variable bound to + the pattern is dependent. We check it for the three kinds of + notations involving bindings of patterns *) + +Check fun '((x,y) as z) => x+y=0/\z=z. (* Primitive fun/forall *) +Check myexists ((x,y) as z), x+y=0/\z=z. (* Isolated binding pattern *) +Check exists '((x,y) as z), x+y=0/\z=z. (* Applicative recursive binder *) +Check ∀ '((x,y) as z), x+y=0/\z=z. (* Other example of recursive binder, now treated as the exists case *) + +(* Check parsability and printability of irrefutable disjunctive patterns *) + +Check fun '(((x,y),true)|((x,y),false)) => x+y. +Check myexists (((x,y),true)|((x,y),false)), x>y. +Check exists '(((x,y),true)|((x,y),false)), x>y. +Check ∀ '(((x,y),true)|((x,y),false)), x>y. + +(* Check Georges' printability of a "if is then else" notation *) + +Notation "'if' c 'is' p 'then' u 'else' v" := + (match c with p => u | _ => v end) + (at level 200, p pattern at level 100). +Check fun p => if p is S n then n else 0. +Check fun p => if p is Lt then 1 else 0. + +(* Check that mixed binders and terms defaults to ident and not pattern *) +Module F. + (* First without an indirection *) +Notation "[ n | t ]" := (n, (fun n : nat => t)). +Check fun S : nat => [ S | S+S ]. +Check fun N : nat => (N, (fun n => n+0)). (* another test in passing *) + (* Then with an indirection *) +Notation "[[ n | p | t ]]" := (n, (fun p : nat => t)). +Notation "[[ n | t ]]" := [[ n | n | t ]]. +Check fun S : nat => [[ S | S+S ]]. +End F. + +(* Check parsability/printability of {x|P} and variants *) + +Check {I:nat|I=I}. +Check {'I:True|I=I}. +Check {'(x,y)|x+y=0}. + +(* Check exists2 with a pattern *) +Check ex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y). diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index 95be04c32c..8a6d94c732 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -31,7 +31,7 @@ exists '(x, y) '(z, w), swap (x, y) = (z, w) : Prop both_z = fun pat : nat * nat => -let '(n, p) as pat0 := pat return (F pat0) in (Z n, Z p) : F (n, p) +let '(n, p) as x := pat return (F x) in (Z n, Z p) : F (n, p) : forall pat : nat * nat, F pat fun '(x, y) '(z, t) => swap (x, y) = (z, t) : A * B -> B * A -> Prop @@ -39,3 +39,9 @@ forall '(x, y) '(z, t), swap (x, y) = (z, t) : Prop fun (pat : nat) '(x, y) => x + y = pat : nat -> nat * nat -> Prop +f = fun x : nat => x + x + : nat -> nat + +Argument scope is [nat_scope] +fun x : nat => x + x + : nat -> nat diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v index 0bad472f41..d671053c07 100644 --- a/test-suite/output/PatternsInBinders.v +++ b/test-suite/output/PatternsInBinders.v @@ -67,3 +67,8 @@ End Suboptimal. (** Test risk of collision for internal name *) Check fun pat => fun '(x,y) => x+y = pat. + +(** Test name in degenerate case *) +Definition f 'x := x+x. +Print f. +Check fun 'x => x+x. diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v index 08918981a4..a498db3e89 100644 --- a/test-suite/output/PrintInfos.v +++ b/test-suite/output/PrintInfos.v @@ -26,6 +26,7 @@ About bar. Print bar. About Peano. (* Module *) +Set Warnings "-deprecated". About existS2. (* Notation *) Arguments eq_refl {A} {x}, {A} x. diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index 45ff5e73b6..b0ac9ea29f 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -12,32 +12,37 @@ Nat.ltb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool Nat.eqb: nat -> nat -> bool Nat.two: nat -Nat.zero: nat Nat.one: nat +Nat.zero: nat O: nat -Nat.double: nat -> nat -Nat.sqrt: nat -> nat Nat.div2: nat -> nat Nat.log2: nat -> nat +Nat.succ: nat -> nat +Nat.sqrt: nat -> nat Nat.pred: nat -> nat +Nat.double: nat -> nat Nat.square: nat -> nat S: nat -> nat -Nat.succ: nat -> nat Nat.ldiff: nat -> nat -> nat -Nat.add: nat -> nat -> nat -Nat.lor: nat -> nat -> nat -Nat.lxor: nat -> nat -> nat +Nat.tail_add: nat -> nat -> nat Nat.land: nat -> nat -> nat -Nat.mul: nat -> nat -> nat -Nat.sub: nat -> nat -> nat -Nat.max: nat -> nat -> nat +Nat.tail_mul: nat -> nat -> nat Nat.div: nat -> nat -> nat -Nat.pow: nat -> nat -> nat -Nat.min: nat -> nat -> nat -Nat.modulo: nat -> nat -> nat +Nat.lor: nat -> nat -> nat Nat.gcd: nat -> nat -> nat -Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat +Nat.modulo: nat -> nat -> nat +Nat.max: nat -> nat -> nat +Nat.sub: nat -> nat -> nat +Nat.mul: nat -> nat -> nat +Nat.lxor: nat -> nat -> nat +Nat.add: nat -> nat -> nat +Nat.min: nat -> nat -> nat +Nat.pow: nat -> nat -> nat +Nat.of_uint: Decimal.uint -> nat +Nat.tail_addmul: nat -> nat -> nat -> nat +Nat.of_uint_acc: Decimal.uint -> nat -> nat Nat.log2_iter: nat -> nat -> nat -> nat -> nat +Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat length: forall A : Type, list A -> nat Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat Nat.div2: nat -> nat @@ -53,14 +58,18 @@ Nat.pow: nat -> nat -> nat Nat.land: nat -> nat -> nat Nat.lxor: nat -> nat -> nat Nat.div: nat -> nat -> nat -Nat.mul: nat -> nat -> nat -Nat.min: nat -> nat -> nat +Nat.lor: nat -> nat -> nat +Nat.tail_mul: nat -> nat -> nat Nat.modulo: nat -> nat -> nat Nat.sub: nat -> nat -> nat -Nat.lor: nat -> nat -> nat +Nat.mul: nat -> nat -> nat Nat.gcd: nat -> nat -> nat Nat.max: nat -> nat -> nat +Nat.tail_add: nat -> nat -> nat Nat.add: nat -> nat -> nat +Nat.min: nat -> nat -> nat +Nat.tail_addmul: nat -> nat -> nat -> nat +Nat.of_uint_acc: Decimal.uint -> nat -> nat Nat.log2_iter: nat -> nat -> nat -> nat -> nat Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat diff --git a/test-suite/output/bug6821.out b/test-suite/output/bug6821.out new file mode 100644 index 0000000000..7b12b53200 --- /dev/null +++ b/test-suite/output/bug6821.out @@ -0,0 +1,2 @@ +forall f : nat -> Type, f x where x : nat := 1 + : Type diff --git a/test-suite/output/bug6821.v b/test-suite/output/bug6821.v new file mode 100644 index 0000000000..40627e331e --- /dev/null +++ b/test-suite/output/bug6821.v @@ -0,0 +1,8 @@ +(* Was failing at printing time with stack overflow due to an infinite + eta-expansion *) + +Notation "x 'where' y .. z := v " := + ((fun y => .. ((fun z => x) v) ..) v) + (at level 11, v at next level, y binder, z binder). + +Check forall f, f x where x := 1. diff --git a/test-suite/output/load/Load_noproof.v b/test-suite/output/load/Load_noproof.v new file mode 100644 index 0000000000..aaf1ffe26d --- /dev/null +++ b/test-suite/output/load/Load_noproof.v @@ -0,0 +1 @@ +Definition f := 2. diff --git a/test-suite/output/load/Load_openproof.v b/test-suite/output/load/Load_openproof.v new file mode 100644 index 0000000000..204d4ecbfe --- /dev/null +++ b/test-suite/output/load/Load_openproof.v @@ -0,0 +1 @@ +Lemma k : True. diff --git a/test-suite/output/load/Load_proof.v b/test-suite/output/load/Load_proof.v new file mode 100644 index 0000000000..e47f66a193 --- /dev/null +++ b/test-suite/output/load/Load_proof.v @@ -0,0 +1,2 @@ +Lemma u : True. +Proof. exact I. Qed. diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v index 82b51b1ffb..36fecf7204 100644 --- a/test-suite/success/Check.v +++ b/test-suite/success/Check.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * 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) *) (************************************************************************) (* Compiling the theories allows testing parsing and typing but not printing *) (* This file tests that pretty-printing does not fail *) diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v index 018b22c489..fdf7797d4b 100644 --- a/test-suite/success/Field.v +++ b/test-suite/success/Field.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * 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) *) (************************************************************************) (**** Tests of Field with real numbers ****) diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 2655b651a0..7c2cf3ee52 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -92,16 +92,37 @@ Check ##### 0 _ 0%bool 0%bool : prod' bool bool. Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end. (* 10. Check computation of binding variable through other notations *) -(* i should be detected as binding variable and the scopes not being checked *) - +(* it should be detected as binding variable and the scopes not being checked *) Notation "'FUNNAT' i => t" := (fun i : nat => i = t) (at level 200). Notation "'Funnat' i => t" := (FUNNAT i => t + i%nat) (at level 200). (* 11. Notations with needed factorization of a recursive pattern *) (* See https://github.com/coq/coq/issues/6078#issuecomment-342287412 *) -Module A. +Module M11. Notation "[:: x1 ; .. ; xn & s ]" := (cons x1 .. (cons xn s) ..). Notation "[:: x1 ; .. ; xn ]" := (cons x1 .. (cons xn nil) ..). Check [:: 1 ; 2 ; 3 ]. Check [:: 1 ; 2 ; 3 & nil ]. (* was failing *) -End A. +End M11. + +(* 12. Preventively check that a variable which does not occur can be instantiated *) +(* by any term. In particular, it should not be restricted to a binder *) +Module M12. +Notation "N ++ x" := (S x) (only parsing). +Check 2 ++ 0. +End M12. + +(* 13. Check that internal data about associativity are not used in comparing levels *) +Module M13. +Notation "x ;; z" := (x + z) + (at level 100, z at level 200, only parsing, right associativity). +Notation "x ;; z" := (x * z) + (at level 100, z at level 200, only parsing) : foo_scope. +End M13. + +(* 14. Check that a notation with a "ident" binder does not include a pattern *) +Module M14. +Notation "'myexists' x , p" := (ex (fun x => p)) + (at level 200, x ident, p at level 200, right associativity) : type_scope. +Check myexists I, I = 0. (* Should not be seen as a constructor *) +End M14. diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v index bffd96044d..7d01d3b07b 100644 --- a/test-suite/success/Tauto.v +++ b/test-suite/success/Tauto.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * 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/success/TestRefine.v b/test-suite/success/TestRefine.v index 87296744c4..f1683078cb 100644 --- a/test-suite/success/TestRefine.v +++ b/test-suite/success/TestRefine.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * 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) *) (************************************************************************) (************************************************************************) diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v index 1fb3abfe41..e05762477d 100644 --- a/test-suite/success/cumulativity.v +++ b/test-suite/success/cumulativity.v @@ -124,3 +124,13 @@ Inductive Mut1 A := with Mut2 A := | Base2 : Type -> Mut2 A | Node2 : Mut1 A -> Mut2 A. + +(* If we don't reduce T while inferring cumulativity for the + constructor we will see a Rel and believe i is irrelevant. *) +Inductive withparams@{i j} (T:=Type@{i}:Type@{j}) := mkwithparams : T -> withparams. + +Definition withparams_co@{i i' j|i < i', i' < j} : withparams@{i j} -> withparams@{i' j} + := fun x => x. + +Fail Definition withparams_not_irr@{i i' j|i' < i, i' < j} : withparams@{i j} -> withparams@{i' j} + := fun x => x. diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v index 9b0ff1c8fe..c44747379f 100644 --- a/test-suite/success/eauto.v +++ b/test-suite/success/eauto.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * 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) *) (************************************************************************) Class A (A : Type). diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v index 055434df01..9b3fb3c5c7 100644 --- a/test-suite/success/eqdecide.v +++ b/test-suite/success/eqdecide.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * 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) *) (************************************************************************) Inductive T : Set := diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index 83726bfdc5..95ae070940 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * 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) *) (************************************************************************) Require Coq.extraction.Extraction. diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v index 7e9095dfd7..92fd6cb17d 100644 --- a/test-suite/success/inds_type_sec.v +++ b/test-suite/success/inds_type_sec.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * 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) *) (************************************************************************) Section S. Inductive T (U : Type) : Type := diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 35d7929877..da7df69e62 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * 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) *) (************************************************************************) (* Test des definitions inductives imbriquees *) diff --git a/test-suite/success/letproj.v b/test-suite/success/letproj.v index a183be6223..de2857b437 100644 --- a/test-suite/success/letproj.v +++ b/test-suite/success/letproj.v @@ -1,5 +1,5 @@ Set Primitive Projections. -Set Record Elimination Schemes. +Set Nonrecursive Elimination Schemes. Record Foo (A : Type) := { bar : A -> A; baz : A }. Definition test (A : Type) (f : Foo A) := diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v index c4c5623897..2c76a13597 100644 --- a/test-suite/success/mutual_ind.v +++ b/test-suite/success/mutual_ind.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * 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 mutuellement inductive et dependante *) diff --git a/test-suite/success/old_typeclass.v b/test-suite/success/old_typeclass.v deleted file mode 100644 index 01e35810b0..0000000000 --- a/test-suite/success/old_typeclass.v +++ /dev/null @@ -1,13 +0,0 @@ -Require Import Setoid Coq.Classes.Morphisms. -Set Typeclasses Legacy Resolution. - -Declare Instance and_Proper_eq: Proper (Logic.eq ==> Logic.eq ==> Logic.eq) and. - -Axiom In : Prop. -Axiom union_spec : In <-> True. - -Lemma foo : In /\ True. -Proof. -progress rewrite union_spec. -repeat constructor. -Qed. diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 576bdbf71b..31a1608c4d 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -1,5 +1,5 @@ Set Primitive Projections. -Set Record Elimination Schemes. +Set Nonrecursive Elimination Schemes. Module Prim. Record F := { a : nat; b : a = a }. diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v index 62249666b3..448d0082db 100644 --- a/test-suite/success/rewrite.v +++ b/test-suite/success/rewrite.v @@ -151,10 +151,25 @@ Abort. (* Check that rewriting within evars still work (was broken in 8.5beta1) *) - Goal forall (a: unit) (H: a = tt), exists x y:nat, x = y. intros; eexists; eexists. rewrite H. Undo. subst. Abort. + +(* Check that iterated rewriting does not rewrite in the side conditions *) +(* Example from Sigurd Schneider, extracted from contrib containers *) + +Lemma EQ + : forall (e e' : nat), True -> e = e'. +Admitted. + +Lemma test (v1 v2 v3: nat) (v' : v1 = v2) : v2 = v1. +Proof. + rewrite <- (EQ v1 v2) in *. + exact v'. + (* There should be only two side conditions *) + exact I. + exact I. +Qed. diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index ce1c33fc40..de8aa252b8 100644 --- a/test-suite/success/unfold.v +++ b/test-suite/success/unfold.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * 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) *) (************************************************************************) (* Test le Hint Unfold sur des var locales *) diff --git a/test-suite/success/vm_evars.v b/test-suite/success/vm_evars.v new file mode 100644 index 0000000000..2c8b099ef0 --- /dev/null +++ b/test-suite/success/vm_evars.v @@ -0,0 +1,23 @@ +Fixpoint iter {A} (n : nat) (f : A -> A) (x : A) := +match n with +| 0 => x +| S n => iter n f (f x) +end. + +Goal nat -> True. +Proof. +intros n. +evar (f : nat -> nat). +cut (iter 10 f 0 = 0). +vm_compute. +intros; constructor. +instantiate (f := (fun x => x)). +reflexivity. +Qed. + +Goal exists x, x = 5 + 5. +Proof. + eexists. + vm_compute. + reflexivity. +Qed. diff --git a/test-suite/typeclasses/NewSetoid.v b/test-suite/typeclasses/NewSetoid.v index 37d197a15c..81c4a1469c 100644 --- a/test-suite/typeclasses/NewSetoid.v +++ b/test-suite/typeclasses/NewSetoid.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * 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) *) (************************************************************************) (* Certified Haskell Prelude. |