diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-03-08 15:30:06 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-03-08 15:30:06 +0000 |
| commit | 32535b28bd75852101541dbd77275d27ff236326 (patch) | |
| tree | 4049bf00345761fe823822e1d850a0365895dc52 /contrib | |
| parent | 35e7236b1c5423b67498e164a0511f961a67056b (diff) | |
Create a program_scope in subtac Utils
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9692 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/subtac/Utils.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v index 686a5fd41..0a28ac45b 100644 --- a/contrib/subtac/Utils.v +++ b/contrib/subtac/Utils.v @@ -64,3 +64,9 @@ Extract Inductive prod => "pair" [ "" ]. Extract Inductive sigT => "pair" [ "" ]. Require Export ProofIrrelevance. + +Delimit Scope program_scope with program. + +Require Import Specif. +Notation "'left'" := (left _ _) : program_scope. +Notation "'right'" := (right _ _) : program_scope. |