diff options
| -rw-r--r-- | pretyping/reductionops.ml | 4 | ||||
| -rw-r--r-- | test-suite/success/polymorphism.v | 16 |
2 files changed, 19 insertions, 1 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index dd671f111e..dc70f36ccf 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1287,7 +1287,9 @@ let sigma_compare_sorts env pb s0 s1 sigma = let sigma_compare_instances flex i0 i1 sigma = try Evd.set_eq_instances ~flex sigma i0 i1 - with Evd.UniversesDiffer -> raise Reduction.NotConvertible + with Evd.UniversesDiffer + | Univ.UniverseInconsistency _ -> + raise Reduction.NotConvertible let sigma_univ_state = { Reduction.compare = sigma_compare_sorts; diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 9167c9fcbf..dc22b03f2d 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -292,3 +292,19 @@ Section foo2. Context `{forall A B, Funext A B}. Print Universes. End foo2. + +Module eta. +Set Universe Polymorphism. + +Set Printing Universes. + +Axiom admit : forall A, A. +Record R := {O : Type}. + +Definition RL (x : R@{i}) : $(let u := constr:(Type@{i}:Type@{j}) in exact (R@{j}) )$ := {|O := @O x|}. +Definition RLRL : forall x : R, RL x = RL (RL x) := fun x => eq_refl. +Definition RLRL' : forall x : R, RL x = RL (RL x). + intros. apply eq_refl. +Qed. + +End eta. |