projects
/
coq-hetmet.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
restore HaskWeakToStrong functionality that I broke over the weekend
[coq-hetmet.git]
/
src
/
Extraction.v
diff --git
a/src/Extraction.v
b/src/Extraction.v
index
7391246
..
65f3f2d
100644
(file)
--- a/
src/Extraction.v
+++ b/
src/Extraction.v
@@
-78,7
+78,7
@@
Section core2proof.
* free tyvars in them *)
Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
match coreVarToWeakVar cv with
* free tyvars in them *)
Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
match coreVarToWeakVar cv with
- | WExprVar wev => match weakTypeToType' φ wev ★ with
+ | WExprVar wev => match weakTypeToType'' φ wev ★ with
| Error s => Prelude_error ("Error in top-level xi: " +++ s)
| OK t => t @@ nil
end
| Error s => Prelude_error ("Error in top-level xi: " +++ s)
| OK t => t @@ nil
end