diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-13 20:13:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-13 20:13:10 +0200 |
| commit | cbb41129f15623ba5be50026f930e0435c9f5259 (patch) | |
| tree | a865d2dbdeb2bf628a863af8183741b6a55cc8bc /proofs/clenv.ml | |
| parent | 36f95a197b106b928a3fc99d7ee5904099a654e4 (diff) | |
| parent | bb43103f7ecea16e634d448215f24d6d55d56eb1 (diff) | |
Merge branch 'v8.5'
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 1ef0b087b..78dce0d64 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -491,7 +491,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 (_,_,NotClean _)) as e -> + | PretypeError (_,_,ActualTypeNotCoercible (_,_, + (NotClean _ | ConversionFailed _))) as e -> raise e | e when precatchable_exception e -> TypeNotProcessed, clenv, c |