projects
/
coq-hetmet.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
e490d1c
)
improve error message
author
Adam Megacz
<megacz@cs.berkeley.edu>
Sun, 27 Mar 2011 02:26:01 +0000
(19:26 -0700)
committer
Adam Megacz
<megacz@cs.berkeley.edu>
Sun, 27 Mar 2011 02:26:01 +0000
(19:26 -0700)
src/ExtractionMain.v
patch
|
blob
|
history
diff --git
a/src/ExtractionMain.v
b/src/ExtractionMain.v
index
61993a1
..
05d059a
100644
(file)
--- a/
src/ExtractionMain.v
+++ b/
src/ExtractionMain.v
@@
-100,7
+100,8
@@
Section core2proof.
Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
match coreVarToWeakVar cv with
| WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
- | Error s => Prelude_error ("Error in top-level xi: " +++ s)
+ | Error s => Prelude_error ("Error converting weakType of top-level variable "+++
+ toString cv+++": " +++ s)
| OK t => t @@ nil
end
| WTypeVar _ => Prelude_error "top-level xi got a type variable"