diff options
| author | msozeau | 2009-05-28 20:47:09 +0000 |
|---|---|---|
| committer | msozeau | 2009-05-28 20:47:09 +0000 |
| commit | f89e016e0503e5b4431b99f707fb3abca541ed19 (patch) | |
| tree | 1da7814ddc7a9373b45d4b433c097672f471caaf | |
| parent | 22130b59eb01cafa9e5e1426e507955dafd13c05 (diff) | |
Properly catch sort constraint inconsistency exception in
[base_sort_conv] and revert change in [unify_type].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12153 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |