diff options
Diffstat (limited to 'proofs/clenv.ml')
-rw-r--r-- | proofs/clenv.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 09e77602d..79b331a27 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -459,7 +459,8 @@ let clenv_unify_binding_type clenv c t u = let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in TypeProcessed, { clenv with evd = evd }, c with - | PretypeError (_,_,ActualTypeNotCoercible _) as e -> + | PretypeError (_,_,ActualTypeNotCoercible (_,_, + (NotClean _ | ConversionFailed _))) as e -> raise e | e when precatchable_exception e -> TypeNotProcessed, clenv, c |