From a46ccd71539257bb55dcddd9ae8510856a5c9a16 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 Jul 2012 16:56:28 +0000 Subject: Open Local Scope ---> Local Open Scope, same with Notation and alii git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Program/Basics.v | 2 +- theories/Program/Subset.v | 2 +- theories/Program/Wf.v | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) (limited to 'theories/Program') diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index 7cef5c5ad..f4ca4d680 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -29,7 +29,7 @@ Hint Unfold compose. Notation " g ∘ f " := (compose g f) (at level 40, left associativity) : program_scope. -Open Local Scope program_scope. +Local Open Scope program_scope. (** The non-dependent function space between [A] and [B]. *) diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index 4642021c4..24baf4598 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -10,7 +10,7 @@ Require Import Coq.Program.Utils. Require Import Coq.Program.Equality. -Open Local Scope program_scope. +Local Open Scope program_scope. (** The following tactics implement a poor-man's solution for proof-irrelevance: it tries to factorize every proof of the same proposition in a goal so that equality of such proofs becomes trivial. *) diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index ee0a7451b..8ef1eb4e6 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -12,7 +12,7 @@ Require Import Coq.Init.Wf. Require Import Coq.Program.Utils. Require Import ProofIrrelevance. -Open Local Scope program_scope. +Local Open Scope program_scope. Section Well_founded. Variable A : Type. -- cgit v1.2.3