summaryrefslogtreecommitdiff
path: root/theories/Classes
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Classes')
-rw-r--r--theories/Classes/CEquivalence.v10
-rw-r--r--theories/Classes/CMorphisms.v12
-rw-r--r--theories/Classes/CRelationClasses.v14
-rw-r--r--theories/Classes/DecidableClass.v10
-rw-r--r--theories/Classes/EquivDec.v10
-rw-r--r--theories/Classes/Equivalence.v10
-rw-r--r--theories/Classes/Init.v10
-rw-r--r--theories/Classes/Morphisms.v12
-rw-r--r--theories/Classes/Morphisms_Prop.v10
-rw-r--r--theories/Classes/Morphisms_Relations.v10
-rw-r--r--theories/Classes/RelationClasses.v14
-rw-r--r--theories/Classes/RelationPairs.v16
-rw-r--r--theories/Classes/SetoidClass.v10
-rw-r--r--theories/Classes/SetoidDec.v10
-rw-r--r--theories/Classes/SetoidTactics.v10
-rw-r--r--theories/Classes/vo.itarget15
16 files changed, 97 insertions, 86 deletions
diff --git a/theories/Classes/CEquivalence.v b/theories/Classes/CEquivalence.v
index bd01de47..03e611f5 100644
--- a/theories/Classes/CEquivalence.v
+++ b/theories/Classes/CEquivalence.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) *)
(************************************************************************)
(** * Typeclass-based setoids. Definitions on [Equivalence].
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index 1cfca416..09b35ca7 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -1,10 +1,12 @@
-(* -*- coding: utf-8 -*- *)
+(* -*- coding: utf-8; coq-prog-args: ("-coqlib" "../.." "-R" ".." "Coq" "-top" "Coq.Classes.CMorphisms") -*- *)
(************************************************************************)
-(* 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) *)
(************************************************************************)
(** * Typeclass-based morphism definition and standard, minimal instances
diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v
index 3d7ef01f..bc821532 100644
--- a/theories/Classes/CRelationClasses.v
+++ b/theories/Classes/CRelationClasses.v
@@ -1,10 +1,12 @@
(* -*- coding: utf-8 -*- *)
(************************************************************************)
-(* 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) *)
(************************************************************************)
(** * Typeclass-based relations, tactics and standard instances
@@ -305,9 +307,7 @@ Section Binary.
fun x y => sum (R x y) (R' x y).
(** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
-
- Set Automatic Introduction.
-
+
Global Instance relation_equivalence_equivalence :
Equivalence relation_equivalence.
Proof. split; red; unfold relation_equivalence, iffT. firstorder.
diff --git a/theories/Classes/DecidableClass.v b/theories/Classes/DecidableClass.v
index a3b7e311..bffad2b3 100644
--- a/theories/Classes/DecidableClass.v
+++ b/theories/Classes/DecidableClass.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) *)
(************************************************************************)
(** * A typeclass to ease the handling of decidable properties. *)
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 52313735..e9a9d6af 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.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) *)
(************************************************************************)
(** * Decidable equivalences.
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 80b0b7e4..5217aedb 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.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) *)
(************************************************************************)
(** * Typeclass-based setoids. Definitions on [Equivalence].
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index c13b36fd..8a04206b 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.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) *)
(************************************************************************)
(** * Initialization code for typeclasses, setting up the default tactic
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 06511ace..1858ba76 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -1,10 +1,12 @@
-(* -*- coding: utf-8 -*- *)
+(* -*- coding: utf-8; coq-prog-args: ("-coqlib" "../.." "-R" ".." "Coq" "-top" "Coq.Classes.Morphisms") -*- *)
(************************************************************************)
-(* 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) *)
(************************************************************************)
(** * Typeclass-based morphism definition and standard, minimal instances
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index 15900177..8881fda5 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.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) *)
(************************************************************************)
(** * [Proper] instances for propositional connectives.
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index 6048fe06..a3e57501 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.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) *)
(************************************************************************)
(** * Morphism instances for relations.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 11c204da..2ab3af20 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -1,10 +1,12 @@
(* -*- coding: utf-8 -*- *)
(************************************************************************)
-(* 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) *)
(************************************************************************)
(** * Typeclass-based relations, tactics and standard instances
@@ -433,9 +435,7 @@ Section Binary.
@predicate_union (A::A::Tnil) R R'.
(** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
-
- Set Automatic Introduction.
-
+
Global Instance relation_equivalence_equivalence :
Equivalence relation_equivalence.
Proof. exact (@predicate_equivalence_equivalence (A::A::Tnil)). Qed.
diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v
index 8d1c4982..7af2b0fc 100644
--- a/theories/Classes/RelationPairs.v
+++ b/theories/Classes/RelationPairs.v
@@ -1,10 +1,12 @@
-(***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
-(* \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) *)
+(************************************************************************)
(** * Relations over pairs *)
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 4b133a4d..2673a119 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.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) *)
(************************************************************************)
(** * Typeclass-based setoids, tactics and standard instances.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 7201c0b1..f6b240bf 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -1,10 +1,12 @@
(* -*- coding: utf-8 -*- *)
(************************************************************************)
-(* 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) *)
(************************************************************************)
(** * Decidable setoid equality theory.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 190397ae..3fab3c5a 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.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 for typeclass-based setoids.
diff --git a/theories/Classes/vo.itarget b/theories/Classes/vo.itarget
deleted file mode 100644
index 18147f2a..00000000
--- a/theories/Classes/vo.itarget
+++ /dev/null
@@ -1,15 +0,0 @@
-DecidableClass.vo
-Equivalence.vo
-EquivDec.vo
-Init.vo
-Morphisms_Prop.vo
-Morphisms_Relations.vo
-Morphisms.vo
-RelationClasses.vo
-SetoidClass.vo
-SetoidDec.vo
-SetoidTactics.vo
-RelationPairs.vo
-CRelationClasses.vo
-CMorphisms.vo
-CEquivalence.vo
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 08:59:24 +0000