diff options
| author | Pierre-Marie Pédrot | 2014-06-10 20:20:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-06-10 20:20:55 +0200 |
| commit | 186fe5301add12580564f4109b40b326afc481fc (patch) | |
| tree | 1bcb5aa9c8dca9ae2bdb0eab31ee302579f7668c /pretyping | |
| parent | 024ad666b1ccda47b9c23d7d5bf33a84b3218618 (diff) | |
Made explanations for universe inconsistencies optional. They are only used
by the printer anyway.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evd.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 8173e7b972..2041f35bf0 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -412,7 +412,7 @@ let process_universe_constraints univs vars alg templ cstrs = Univ.LSet.fold (fun l local -> if Univ.Level.is_small l || Univ.LMap.mem l !vars then Univ.enforce_eq (Univ.Universe.make l) r local - else raise (Univ.UniverseInconsistency (Univ.Le, Univ.Universe.make l, r, []))) + else raise (Univ.UniverseInconsistency (Univ.Le, Univ.Universe.make l, r, None))) levels local else if Univ.LSet.mem rl templ && Univ.Universe.is_level l then unify_universes fo l Universes.UEq r local @@ -439,7 +439,7 @@ let process_universe_constraints univs vars alg templ cstrs = (* Two rigid/global levels, none of them being local, one of them being Prop/Set, disallow *) if Univ.Level.is_small l' || Univ.Level.is_small r' then - raise (Univ.UniverseInconsistency (Univ.Eq, l, r, [])) + raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) else if fo then raise UniversesDiffer @@ -447,7 +447,7 @@ let process_universe_constraints univs vars alg templ cstrs = Univ.enforce_eq_level l' r' local | _, _ (* One of the two is algebraic or global *) -> if Univ.check_eq univs l r then local - else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, [])) + else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) in let local = Universes.Constraints.fold (fun (l,d,r) local -> unify_universes false l d r local) |