diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-11 00:29:02 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:27:27 +0100 |
| commit | ca993b9e7765ac58f70740818758457c9367b0da (patch) | |
| tree | a813ef9a194638afbb09cefe1d1e2bce113a9d84 /toplevel/explainErr.ml | |
| parent | c2855a3387be134d1220f301574b743572a94239 (diff) | |
Making judgment type generic over the type of inner constrs.
This allows to factorize code and prevents the unnecessary use of back and
forth conversions between the various types of terms.
Note that functions from typing may now raise errors as PretypeError rather
than TypeError, because they call the proper wrapper. I think that they were
wrongly calling the kernel because of an overlook of open modules.
Diffstat (limited to 'toplevel/explainErr.ml')
| -rw-r--r-- | toplevel/explainErr.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/explainErr.ml b/toplevel/explainErr.ml index 17897460c..414087718 100644 --- a/toplevel/explainErr.ml +++ b/toplevel/explainErr.ml @@ -63,6 +63,7 @@ let process_vernac_interp_error with_header exn = match fst exn with mt() in wrap_vernac_error with_header exn (str "Universe inconsistency" ++ msg ++ str ".") | TypeError(ctx,te) -> + let te = Himsg.map_ptype_error EConstr.of_constr te in wrap_vernac_error with_header exn (Himsg.explain_type_error ctx Evd.empty te) | PretypeError(ctx,sigma,te) -> wrap_vernac_error with_header exn (Himsg.explain_pretype_error ctx sigma te) |