diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-30 14:18:34 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-30 14:18:34 +0000 |
| commit | b8018319137599b5809bcce0aafca2ecf96b4bf9 (patch) | |
| tree | 0f1c2671bca0eaa189354b8b845db5c98f0c0a1d /pretyping | |
| parent | 4da1d9ee92f6764e8dee236730652391323a2ec5 (diff) | |
Attempt to capture on time unification errors for "with" bindings.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12450 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/clenv.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index d21c8ad45..9ce46ab8a 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -404,8 +404,10 @@ let clenv_unify_binding_type clenv c t u = try let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in TypeProcessed, { clenv with evd = evd }, c - with e when precatchable_exception e -> - TypeNotProcessed, clenv, c + with + | PretypeError (_,NotClean _) as e -> raise e + | e when precatchable_exception e -> + TypeNotProcessed, clenv, c let clenv_assign_binding clenv k (sigma,c) = let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in |