diff options
Diffstat (limited to 'kernel/univ.ml')
| -rw-r--r-- | kernel/univ.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index d967846f1..e6ecadf31 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -512,7 +512,9 @@ type constraint_function = universe -> universe -> constraints -> constraints let constraint_add_leq v u c = - if v = UniverseLevel.Set then c else Constraint.add (v,Le,u) c + (* We just discard trivial constraints like Set<=u or u<=u *) + if v = UniverseLevel.Set || UniverseLevel.compare v u = 0 then c + else Constraint.add (v,Le,u) c let enforce_geq u v c = match u, v with @@ -524,7 +526,9 @@ let enforce_geq u v c = let enforce_eq u v c = match (u,v) with - | Atom u, Atom v -> Constraint.add (u,Eq,v) c + | Atom u, Atom v -> + (* We discard trivial constraints like u=u *) + if UniverseLevel.compare u v = 0 then c else Constraint.add (u,Eq,v) c | _ -> anomaly "A universe comparison can only happen between variables" let merge_constraints c g = |