diff options
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 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. |