diff options
| author | letouzey | 2012-07-05 16:56:28 +0000 |
|---|---|---|
| committer | letouzey | 2012-07-05 16:56:28 +0000 |
| commit | a46ccd71539257bb55dcddd9ae8510856a5c9a16 (patch) | |
| tree | f5934c98bd6288cc485f20dd9dfeae598170697e /theories/Program | |
| parent | 8e33b709fb2225d256dccfd4b071f85144d92d45 (diff) | |
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
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Basics.v | 2 | ||||
| -rw-r--r-- | theories/Program/Subset.v | 2 | ||||
| -rw-r--r-- | theories/Program/Wf.v | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index 7cef5c5ad8..f4ca4d6808 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 4642021c40..24baf45986 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 ee0a7451bf..8ef1eb4e67 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. |