diff options
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 4e0b6f75e7..4372668fcf 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1074,12 +1074,6 @@ let uctx_new_univ_variable rigid name predicative uctx_univ_algebraic = Univ.LSet.add u avars}, false else {uctx with uctx_univ_variables = uvars'}, false in - (* let ctx' = *) - (* if pred then *) - (* Univ.ContextSet.add_constraints *) - (* (Univ.Constraint.singleton (Univ.Level.set, Univ.Le, u)) ctx' *) - (* else ctx' *) - (* in *) let names = match name with | Some n -> add_uctx_names n u uctx.uctx_names |