diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 8df362f3ac..1cbb47846c 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -928,6 +928,9 @@ let explain_meta_in_type c = str "In refiner, a meta appears in the type " ++ brk(1,1) ++ pr_lconstr c ++ str " of another meta" +let explain_no_such_hyp id = + str "No such hypothesis: " ++ pr_id id + let explain_refiner_error = function | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty | UnresolvedBindings t -> explain_refiner_unresolved_bindings t @@ -937,6 +940,7 @@ let explain_refiner_error = function | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in c hyp | NonLinearProof c -> explain_non_linear_proof c | MetaInType c -> explain_meta_in_type c + | NoSuchHyp id -> explain_no_such_hyp id (* Inductive errors *) |