diff options
| author | Pierre-Marie Pédrot | 2016-08-22 11:11:41 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-08-22 11:12:53 +0200 |
| commit | 687d510cb43db5029fb4545c3b12ac20cf99197a (patch) | |
| tree | 1030e647b3599dc1dcf09dfe55b90f24b126038a | |
| parent | 1948023891d26e628397a303263b912225f2cc31 (diff) | |
Pushing error backtrace in unification reraise.
| -rw-r--r-- | pretyping/unification.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 0c1ce0d2f8..6d80db6455 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1080,8 +1080,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb if !debug_unification then Feedback.msg_debug (str "Leaving unification with success"); a with e -> + let e = CErrors.push e in if !debug_unification then Feedback.msg_debug (str "Leaving unification with failure"); - raise e + iraise e let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env |