diff options
| -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 686a5fd415..0a28ac45ba 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. |