diff src/MoreSpecif.v @ 221:54e8ecb5ec88

Port Reflection
author Adam Chlipala <adamc@hcoop.net>
date Mon, 16 Nov 2009 11:09:47 -0500
parents 5ea9a0bff8f7
children 1f57a8d0ed3d
line wrap: on
line diff
--- a/src/MoreSpecif.v	Mon Nov 16 10:32:04 2009 -0500
+++ b/src/MoreSpecif.v	Mon Nov 16 11:09:47 2009 -0500
@@ -17,7 +17,7 @@
 Notation "x <== e1 ; e2" := (let (x, _) := e1 in e2)
 (right associativity, at level 60) : specif_scope.
 
-Open Local Scope specif_scope.
+Local Open Scope specif_scope.
 Delimit Scope specif_scope with specif.
 
 Notation "'Yes'" := (left _ _) : specif_scope.
@@ -88,7 +88,7 @@
 Notation "'Yes'" := (Proved _) : partial_scope.
 Notation "'No'" := (Uncertain _) : partial_scope.
 
-Open Local Scope partial_scope.
+Local Open Scope partial_scope.
 Delimit Scope partial_scope with partial.
 
 Notation "'Reduce' v" := (if v then Yes else No) : partial_scope.