Mercurial > cpdt > repo
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.