diff options
Diffstat (limited to 'theories/Init')
-rw-r--r-- | theories/Init/Datatypes.v | 28 | ||||
-rw-r--r-- | theories/Init/Decimal.v | 10 | ||||
-rw-r--r-- | theories/Init/Logic.v | 24 | ||||
-rw-r--r-- | theories/Init/Logic_Type.v | 18 | ||||
-rw-r--r-- | theories/Init/Nat.v | 10 | ||||
-rw-r--r-- | theories/Init/Notations.v | 10 | ||||
-rw-r--r-- | theories/Init/Peano.v | 30 | ||||
-rw-r--r-- | theories/Init/Prelude.v | 10 | ||||
-rw-r--r-- | theories/Init/Specif.v | 36 | ||||
-rw-r--r-- | theories/Init/Tactics.v | 10 | ||||
-rw-r--r-- | theories/Init/Wf.v | 10 |
11 files changed, 109 insertions, 87 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 22e10e2e4..05b741f0a 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.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) *) (************************************************************************) Set Implicit Arguments. @@ -359,14 +361,14 @@ Definition idProp : IDProp := fun A x => x. (* Compatibility *) -Notation prodT := prod (compat "8.2"). -Notation pairT := pair (compat "8.2"). -Notation prodT_rect := prod_rect (compat "8.2"). -Notation prodT_rec := prod_rec (compat "8.2"). -Notation prodT_ind := prod_ind (compat "8.2"). -Notation fstT := fst (compat "8.2"). -Notation sndT := snd (compat "8.2"). -Notation prodT_uncurry := prod_uncurry (compat "8.2"). -Notation prodT_curry := prod_curry (compat "8.2"). +Notation prodT := prod (only parsing). +Notation pairT := pair (only parsing). +Notation prodT_rect := prod_rect (only parsing). +Notation prodT_rec := prod_rec (only parsing). +Notation prodT_ind := prod_ind (only parsing). +Notation fstT := fst (only parsing). +Notation sndT := snd (only parsing). +Notation prodT_uncurry := prod_uncurry (only parsing). +Notation prodT_curry := prod_curry (only parsing). (* end hide *) diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v index fa462f147..57163b1b0 100644 --- a/theories/Init/Decimal.v +++ b/theories/Init/Decimal.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) *) (************************************************************************) (** * Decimal numbers *) diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 053ed601f..10ca9ecc9 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.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) *) (************************************************************************) Set Implicit Arguments. @@ -549,14 +551,14 @@ Qed. (* Aliases *) -Notation sym_eq := eq_sym (compat "8.3"). -Notation trans_eq := eq_trans (compat "8.3"). -Notation sym_not_eq := not_eq_sym (compat "8.3"). +Notation sym_eq := eq_sym (only parsing). +Notation trans_eq := eq_trans (only parsing). +Notation sym_not_eq := not_eq_sym (only parsing). -Notation refl_equal := eq_refl (compat "8.3"). -Notation sym_equal := eq_sym (compat "8.3"). -Notation trans_equal := eq_trans (compat "8.3"). -Notation sym_not_equal := not_eq_sym (compat "8.3"). +Notation refl_equal := eq_refl (only parsing). +Notation sym_equal := eq_sym (only parsing). +Notation trans_equal := eq_trans (only parsing). +Notation sym_not_equal := not_eq_sym (only parsing). Hint Immediate eq_sym not_eq_sym: core. diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index 567d2c15c..6f10a9399 100644 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.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 module defines type constructors for types in [Type] @@ -66,7 +68,7 @@ Defined. Hint Immediate identity_sym not_identity_sym: core. -Notation refl_id := identity_refl (compat "8.3"). -Notation sym_id := identity_sym (compat "8.3"). -Notation trans_id := identity_trans (compat "8.3"). -Notation sym_not_id := not_identity_sym (compat "8.3"). +Notation refl_id := identity_refl (only parsing). +Notation sym_id := identity_sym (only parsing). +Notation trans_id := identity_trans (only parsing). +Notation sym_not_id := not_identity_sym (only parsing). diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v index 8f2648269..ad1bc717c 100644 --- a/theories/Init/Nat.v +++ b/theories/Init/Nat.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 Import Notations Logic Datatypes. diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index a9051e761..683a442cb 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.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) *) (************************************************************************) (** These are the notations whose level and associativity are imposed by Coq *) diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 571d2f2dd..73c8c5ef4 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.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) *) (************************************************************************) (** The type [nat] of Peano natural numbers (built from [O] and [S]) @@ -37,7 +39,7 @@ Hint Resolve f_equal_nat: core. (** The predecessor function *) -Notation pred := Nat.pred (compat "8.4"). +Notation pred := Nat.pred (only parsing). Definition f_equal_pred := f_equal pred. @@ -79,7 +81,7 @@ Hint Resolve n_Sn: core. (** Addition *) -Notation plus := Nat.add (compat "8.4"). +Notation plus := Nat.add (only parsing). Infix "+" := Nat.add : nat_scope. Definition f_equal2_plus := f_equal2 plus. @@ -110,12 +112,12 @@ Qed. (** Standard associated names *) -Notation plus_0_r_reverse := plus_n_O (compat "8.2"). -Notation plus_succ_r_reverse := plus_n_Sm (compat "8.2"). +Notation plus_0_r_reverse := plus_n_O (only parsing). +Notation plus_succ_r_reverse := plus_n_Sm (only parsing). (** Multiplication *) -Notation mult := Nat.mul (compat "8.4"). +Notation mult := Nat.mul (only parsing). Infix "*" := Nat.mul : nat_scope. Definition f_equal2_mult := f_equal2 mult. @@ -137,12 +139,12 @@ Hint Resolve mult_n_Sm: core. (** Standard associated names *) -Notation mult_0_r_reverse := mult_n_O (compat "8.2"). -Notation mult_succ_r_reverse := mult_n_Sm (compat "8.2"). +Notation mult_0_r_reverse := mult_n_O (only parsing). +Notation mult_succ_r_reverse := mult_n_Sm (only parsing). (** Truncated subtraction: [m-n] is [0] if [n>=m] *) -Notation minus := Nat.sub (compat "8.4"). +Notation minus := Nat.sub (only parsing). Infix "-" := Nat.sub : nat_scope. (** Definition of the usual orders, the basic properties of [le] and [lt] @@ -219,8 +221,8 @@ Qed. (** Maximum and minimum : definitions and specifications *) -Notation max := Nat.max (compat "8.4"). -Notation min := Nat.min (compat "8.4"). +Notation max := Nat.max (only parsing). +Notation min := Nat.min (only parsing). Lemma max_l n m : m <= n -> Nat.max n m = n. Proof. diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 63c431e8e..802f18c0f 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.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 Export Notations. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 47e8a7558..137bd3a0f 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.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) *) (************************************************************************) (** Basic specifications : sets that may contain logical information *) @@ -742,16 +744,16 @@ Hint Resolve exist exist2 existT existT2: core. (* Compatibility *) -Notation sigS := sigT (compat "8.2"). -Notation existS := existT (compat "8.2"). -Notation sigS_rect := sigT_rect (compat "8.2"). -Notation sigS_rec := sigT_rec (compat "8.2"). -Notation sigS_ind := sigT_ind (compat "8.2"). -Notation projS1 := projT1 (compat "8.2"). -Notation projS2 := projT2 (compat "8.2"). - -Notation sigS2 := sigT2 (compat "8.2"). -Notation existS2 := existT2 (compat "8.2"). -Notation sigS2_rect := sigT2_rect (compat "8.2"). -Notation sigS2_rec := sigT2_rec (compat "8.2"). -Notation sigS2_ind := sigT2_ind (compat "8.2"). +Notation sigS := sigT (compat "8.6"). +Notation existS := existT (compat "8.6"). +Notation sigS_rect := sigT_rect (compat "8.6"). +Notation sigS_rec := sigT_rec (compat "8.6"). +Notation sigS_ind := sigT_ind (compat "8.6"). +Notation projS1 := projT1 (compat "8.6"). +Notation projS2 := projT2 (compat "8.6"). + +Notation sigS2 := sigT2 (compat "8.6"). +Notation existS2 := existT2 (compat "8.6"). +Notation sigS2_rect := sigT2_rect (compat "8.6"). +Notation sigS2_rec := sigT2_rec (compat "8.6"). +Notation sigS2_ind := sigT2_ind (compat "8.6"). diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 47a971ef0..9e6c26b10 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.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 Import Notations. diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 690a3f644..c27ffa33f 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.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 module proves the validity of |