projects
/
coq-hetmet.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
NaturalDeduction: allow multi-rule implementations for SequentExpansion and TreeStruc...
[coq-hetmet.git]
/
src
/
HaskCoreToWeak.v
diff --git
a/src/HaskCoreToWeak.v
b/src/HaskCoreToWeak.v
index
6e1b58f
..
abcd6b8
100644
(file)
--- a/
src/HaskCoreToWeak.v
+++ b/
src/HaskCoreToWeak.v
@@
-53,7
+53,7
@@
Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
| WExprVar _ => Error "encountered expression variable in a modal box type"
| WCoerVar _ => Error "encountered coercion variable in a modal box type"
end
| WExprVar _ => Error "encountered expression variable in a modal box type"
| WCoerVar _ => Error "encountered coercion variable in a modal box type"
end
- | _ => Error ("mis-applied modal box tycon: " +++ ct)
+ | _ => Error ("mis-applied modal box tycon: " +++ toString ct)
end
else let tc' := if eqd_dec tc ArrowTyCon
then WFunTyCon
end
else let tc' := if eqd_dec tc ArrowTyCon
then WFunTyCon
@@
-134,8
+134,8
@@
Fixpoint expectTyConApp (wt:WeakType)(acc:list WeakType) : ???(TyCon * list Weak
match wt with
| WTyCon tc => OK (tc,acc)
| WAppTy t1 t2 => expectTyConApp t1 (t2::acc)
match wt with
| WTyCon tc => OK (tc,acc)
| WAppTy t1 t2 => expectTyConApp t1 (t2::acc)
- | WTyFunApp tc tys => Error ("expectTyConApp encountered TyFunApp: " +++ wt)
- | _ => Error ("expectTyConApp encountered " +++ wt)
+ | WTyFunApp tc tys => Error ("expectTyConApp encountered TyFunApp: " +++ toString wt)
+ | _ => Error ("expectTyConApp encountered " +++ toString wt)
end.
Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
end.
Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=