diff options
| -rw-r--r-- | pretyping/evarconv.ml | 4 | ||||
| -rw-r--r-- | pretyping/unification.ml | 6 |
2 files changed, 8 insertions, 2 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 0d5df1615c..a7c978168f 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -25,7 +25,8 @@ open Libnames open Evd let base_sort_conv evd pb s1 s2 = - match (s1,s2) with + try + match (s1,s2) with | (Prop c1, Prop c2) -> if c1 = Null or c2 = Pos then Some evd else None (* Prop <= Set *) | (Prop c1, Type u) -> if pb = Reduction.CUMUL then Some evd @@ -40,6 +41,7 @@ let base_sort_conv evd pb s1 s2 = match pb with | CONV -> Some (Evd.set_eq_sort_variable evd s1 s2) | CUMUL -> Some (Evd.set_leq_sort_variable evd s1 s2) + with e -> None let unify_constr_univ evd f cv_pb t1 t2 = match kind_of_term t1, kind_of_term t2 with diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 85ca0917d8..0f8d2b860a 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -573,7 +573,11 @@ let unify_to_type env sigma flags c status u = unify_0 env sigma Cumul flags u t else if status = IsSubType then unify_0 env sigma Cumul flags t u - else unify_0 env sigma topconv flags t u + else (* If the terms were convertible under an app, + the types could be in any inclusion order *) + try unify_0 env sigma Cumul flags t u + with ex when precatchable_exception ex -> + unify_0 env sigma Cumul flags u t let unify_type env sigma flags mv status c = let mvty = Typing.meta_type sigma mv in |