aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pretype_errors.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-05-16 13:57:58 +0200
committerPierre-Marie Pédrot2020-05-16 13:57:58 +0200
commitebaaa7371c3a3548ccec1836621726f6d829858a (patch)
treef5bfbfa5ad485e7c2f7b680de794b2005506bef9 /pretyping/pretype_errors.mli
parent2111994285a21df662c232fa5acfd60e8a640795 (diff)
parent8fd01b538c5b4ea58eecf8be07ab8115619cca4d (diff)
Merge PR #11566: [misc] Better preserve backtraces in several modules
Ack-by: SkySkimmer Reviewed-by: ppedrot
Diffstat (limited to 'pretyping/pretype_errors.mli')
-rw-r--r--pretyping/pretype_errors.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 7086584642..70f218d617 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -75,7 +75,7 @@ val precatchable_exception : exn -> bool
(** Raising errors *)
val error_actual_type :
- ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr ->
+ ?loc:Loc.t -> ?info:Exninfo.info -> env -> Evd.evar_map -> unsafe_judgment -> constr ->
unification_error -> 'b
val error_actual_type_core :