diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-17 18:09:48 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-19 18:52:13 +0100 |
| commit | 090fffa57b2235f70d4355f5dc85d73fa2634655 (patch) | |
| tree | d07b76c4f97d2c1266563ccdb8f5ee1c86143054 /pretyping/evd.ml | |
| parent | 51c8b16816ad0e9bdfaab0314fa6a0db5f4528f5 (diff) | |
Option -type-in-type continued (deactivate test for inferred sort of
inductive types + deactivate test for equality of sort + deactivate
the check that the constraints Prop/Set <= Type are declared).
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index d36a6a20f..d5e3c6715 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1114,12 +1114,16 @@ let normalize_sort evars s = if u' == u then s else Type u' (* FIXME inefficient *) -let set_eq_sort d s1 s2 = +let set_eq_sort env d s1 s2 = let s1 = normalize_sort d s1 and s2 = normalize_sort d s2 in match is_eq_sort s1 s2 with | None -> d - | Some (u1, u2) -> add_universe_constraints d - (Universes.Constraints.singleton (u1,Universes.UEq,u2)) + | Some (u1, u2) -> + if not (type_in_type env) then + add_universe_constraints d + (Universes.Constraints.singleton (u1,Universes.UEq,u2)) + else + d let has_lub evd u1 u2 = (* let normalize = Universes.normalize_universe_opt_subst (ref univs.uctx_univ_variables) in *) |