projects
/
helm.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
9c9ac71
)
print few more wired assertions
author
Enrico Tassi
<enrico.tassi@inria.fr>
Thu, 30 Aug 2007 13:10:22 +0000
(13:10 +0000)
committer
Enrico Tassi
<enrico.tassi@inria.fr>
Thu, 30 Aug 2007 13:10:22 +0000
(13:10 +0000)
helm/software/matita/matitaExcPp.ml
patch
|
blob
|
history
diff --git
a/helm/software/matita/matitaExcPp.ml
b/helm/software/matita/matitaExcPp.ml
index c3c78929ff8e978eae839c1cf7cf677940df4778..339971feaed0d33f73339bb3ce6e25244369cf48 100644
(file)
--- a/
helm/software/matita/matitaExcPp.ml
+++ b/
helm/software/matita/matitaExcPp.ml
@@
-56,7
+56,8
@@
let rec to_string =
| Continuationals.Error s -> None, "Tactical error: " ^ Lazy.force s
| ProofEngineHelpers.Bad_pattern msg ->
None, "Bad pattern: " ^ Lazy.force msg
- | CicRefine.RefineFailure msg ->
+ | CicRefine.RefineFailure msg
+ | CicRefine.AssertFailure msg ->
None, "Refiner error: " ^ Lazy.force msg
| CicTypeChecker.TypeCheckerFailure msg ->
None, "Type checking error: " ^ Lazy.force msg