summaryrefslogtreecommitdiff
path: root/theories/Classes
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Classes')
-rw-r--r--theories/Classes/EquivDec.v4
-rw-r--r--theories/Classes/Equivalence.v6
-rw-r--r--theories/Classes/Init.v2
-rw-r--r--theories/Classes/Morphisms.v4
-rw-r--r--theories/Classes/Morphisms_Prop.v2
-rw-r--r--theories/Classes/Morphisms_Relations.v2
-rw-r--r--theories/Classes/RelationClasses.v4
-rw-r--r--theories/Classes/SetoidClass.v2
-rw-r--r--theories/Classes/SetoidDec.v4
-rw-r--r--theories/Classes/SetoidTactics.v4
10 files changed, 17 insertions, 17 deletions
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 719a9a84..cb1bdb1d 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -49,7 +49,7 @@ Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
| right H => @left _ _ H
end.
-Open Local Scope program_scope.
+Local Open Scope program_scope.
(** Invert the branches. *)
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index d9e9fe25..e0f5a395 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -26,7 +26,7 @@ Unset Strict Implicit.
Generalizable Variables A R eqA B S eqB.
Local Obligation Tactic := simpl_relation.
-Open Local Scope signature_scope.
+Local Open Scope signature_scope.
Definition equiv `{Equivalence A R} : relation A := R.
@@ -37,7 +37,7 @@ Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scop
Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope.
-Open Local Scope equiv_scope.
+Local Open Scope equiv_scope.
(** Overloading for [PER]. *)
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index a001f2e9..06730095 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 8e491b1b..617ff190 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -1,7 +1,7 @@
(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -73,7 +73,7 @@ End ProperNotations.
Export ProperNotations.
-Open Local Scope signature_scope.
+Local Open Scope signature_scope.
(** [solve_proper] try to solve the goal [Proper (?==> ... ==>?) f]
by repeated introductions and setoid rewrites. It should work
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index 256bcc37..2252e42f 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index 7ac49eeb..ea2afb30 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index cf05d9d4..71647953 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -1,7 +1,7 @@
(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -286,7 +286,7 @@ Definition predicate_implication {l : Tlist} :=
Infix "<∙>" := predicate_equivalence (at level 95, no associativity) : predicate_scope.
Infix "-∙>" := predicate_implication (at level 70, right associativity) : predicate_scope.
-Open Local Scope predicate_scope.
+Local Open Scope predicate_scope.
(** The pointwise liftings of conjunction and disjunctions.
Note that these are [binary_operation]s, building new relations out of old ones. *)
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 591671d9..6efc2302 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 6708220e..ac1e1dc4 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -1,7 +1,7 @@
(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -50,7 +50,7 @@ Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
Require Import Coq.Program.Program.
-Open Local Scope program_scope.
+Local Open Scope program_scope.
(** Invert the branches. *)
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 31a4f5f2..fa939e22 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -146,7 +146,7 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y)
Require Import Coq.Program.Tactics.
-Open Local Scope signature_scope.
+Local Open Scope signature_scope.
Ltac red_subst_eq_morphism concl :=
match concl with
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 12:53:38 +0000