Commit e80dd529 authored by Adam Chlipala's avatar Adam Chlipala

Port Reflection

parent 5166e535
...@@ -487,7 +487,7 @@ Module PatMatch. ...@@ -487,7 +487,7 @@ Module PatMatch.
Delimit Scope source_scope with source. Delimit Scope source_scope with source.
Bind Scope source_scope with exp. Bind Scope source_scope with exp.
Open Local Scope source_scope. Local Open Scope source_scope.
Fixpoint typeDenote (t : type) : Set := Fixpoint typeDenote (t : type) : Set :=
match t with match t with
...@@ -728,7 +728,7 @@ Module PatMatch. ...@@ -728,7 +728,7 @@ Module PatMatch.
Implicit Arguments merge [var t result]. Implicit Arguments merge [var t result].
Section elaborate. Section elaborate.
Open Local Scope elab_scope. Local Open Scope elab_scope.
Fixpoint elaboratePat var t1 ts result (p : pat t1 ts) {struct p} : Fixpoint elaboratePat var t1 ts result (p : pat t1 ts) {struct p} :
(hlist (exp var) ts -> result) -> result -> choice_tree var t1 result := (hlist (exp var) ts -> result) -> result -> choice_tree var t1 result :=
......
...@@ -17,7 +17,7 @@ Notation "[ e ]" := (exist _ e _) : specif_scope. ...@@ -17,7 +17,7 @@ Notation "[ e ]" := (exist _ e _) : specif_scope.
Notation "x <== e1 ; e2" := (let (x, _) := e1 in e2) Notation "x <== e1 ; e2" := (let (x, _) := e1 in e2)
(right associativity, at level 60) : specif_scope. (right associativity, at level 60) : specif_scope.
Open Local Scope specif_scope. Local Open Scope specif_scope.
Delimit Scope specif_scope with specif. Delimit Scope specif_scope with specif.
Notation "'Yes'" := (left _ _) : specif_scope. Notation "'Yes'" := (left _ _) : specif_scope.
...@@ -88,7 +88,7 @@ Notation "[ P ]" := (partial P) : type_scope. ...@@ -88,7 +88,7 @@ Notation "[ P ]" := (partial P) : type_scope.
Notation "'Yes'" := (Proved _) : partial_scope. Notation "'Yes'" := (Proved _) : partial_scope.
Notation "'No'" := (Uncertain _) : partial_scope. Notation "'No'" := (Uncertain _) : partial_scope.
Open Local Scope partial_scope. Local Open Scope partial_scope.
Delimit Scope partial_scope with partial. Delimit Scope partial_scope with partial.
Notation "'Reduce' v" := (if v then Yes else No) : partial_scope. Notation "'Reduce' v" := (if v then Yes else No) : partial_scope.
......
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment