diff options
| -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 |