diff options
| author | letouzey | 2008-04-17 16:29:49 +0000 |
|---|---|---|
| committer | letouzey | 2008-04-17 16:29:49 +0000 |
| commit | bc69d8fe0d3585036b1de6d4b43ad80fe49af028 (patch) | |
| tree | fdeb6bab85d5f68977da8ce0aae4dc23a6de031c /theories/FSets | |
| parent | cde0f764b75f25526005d078e17a5ef5d52301f1 (diff) | |
Prevent the apparition of &&& when printing a (if ... then ... else false)
and idem for |||, thanks to a specific scope lazy_bool_scope.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10811 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/FSets')
| -rw-r--r-- | theories/FSets/FMapAVL.v | 1 | ||||
| -rw-r--r-- | theories/FSets/FSetAVL.v | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 521fd13d82..2a2960f19e 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -36,6 +36,7 @@ Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. Module Raw (Import I:Int)(X: OrderedType). Open Local Scope pair_scope. +Open Local Scope lazy_bool_scope. Open Local Scope Int_scope. Definition key := X.t. diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v index faf12cea7d..6a1e07185a 100644 --- a/theories/FSets/FSetAVL.v +++ b/theories/FSets/FSetAVL.v @@ -54,6 +54,7 @@ Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. Module Raw (Import I:Int)(X:OrderedType). Open Local Scope pair_scope. +Open Local Scope lazy_bool_scope. Open Local Scope Int_scope. Definition elt := X.t. |