diff options
| author | barras | 2012-10-17 02:35:08 +0000 |
|---|---|---|
| committer | barras | 2012-10-17 02:35:08 +0000 |
| commit | 9834fe8ac933230607eb33c9cbbaa68a7b13f4fe (patch) | |
| tree | eba7cac3370d517aa0bf48a76e383a902426e894 /pretyping | |
| parent | 927b92eb8e1abf7ff1978f812b602b276d69dd27 (diff) | |
univ inconsistency error message gives evidence of a cycle
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15898 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evd.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index cc6bd61505..dab4ee9c79 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -522,15 +522,15 @@ let set_leq_sort ({evars = (sigma, (us, sm))} as d) s1 s2 = match s1, s2 with | Prop c, Prop c' -> if c = Null && c' = Pos then d - else (raise (Univ.UniverseInconsistency (Univ.Le, u1, u2))) + else (raise (Univ.UniverseInconsistency (Univ.Le, u1, u2,[]))) | Type u, Prop c -> if c = Pos then add_constraints d (Univ.enforce_leq u Univ.type0_univ Univ.empty_constraint) - else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2)) + else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2,[])) | _, Type u -> if is_univ_var_or_set u then add_constraints d (Univ.enforce_leq u1 u2 Univ.empty_constraint) - else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2)) + else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2,[])) let is_univ_level_var us u = match Univ.universe_level u with @@ -553,7 +553,7 @@ let set_eq_sort ({evars = (sigma, (us, sm))} as d) s1 s2 = | Type u, Prop c when is_univ_var_or_set u && Univ.check_eq sm u1 u2 -> d | Type u, Type v when is_univ_var_or_set u && is_univ_var_or_set v -> add_constraints d (Univ.enforce_eq u1 u2 Univ.empty_constraint) - | _, _ -> raise (Univ.UniverseInconsistency (Univ.Eq, u1, u2)) + | _, _ -> raise (Univ.UniverseInconsistency (Univ.Eq, u1, u2, [])) (**********************************************************) (* Accessing metas *) |