Mercurial > cpdt > repo

diff src/Extensional.v @ 221:54e8ecb5ec88

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Port Reflection
author Adam Chlipala <adamc@hcoop.net>
date Mon, 16 Nov 2009 11:09:47 -0500
parents d1464997078d
children 4b73ea13574d
line wrap: on
line diff
--- a/src/Extensional.v	Mon Nov 16 10:32:04 2009 -0500
+++ b/src/Extensional.v	Mon Nov 16 11:09:47 2009 -0500
@@ -487,7 +487,7 @@
     Delimit Scope source_scope with source.
     Bind Scope source_scope with exp.
 
-    Open Local Scope source_scope.
+    Local Open Scope source_scope.
 
     Fixpoint typeDenote (t : type) : Set :=
       match t with
@@ -728,7 +728,7 @@
   Implicit Arguments merge [var t result].
 
   Section elaborate.
-    Open Local Scope elab_scope.
+    Local Open Scope elab_scope.
 
     Fixpoint elaboratePat var t1 ts result (p : pat t1 ts) {struct p} :
       (hlist (exp var) ts -> result) -> result -> choice_tree var t1 result :=