diff options
| author | Maxime Dénès | 2015-10-27 23:59:05 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2015-10-28 16:57:55 +0100 |
| commit | 90dfacaacfec8265b11dc9291de9510f515c0081 (patch) | |
| tree | 7cdf561c5f7a8df718152b37a2943776892f76e3 /pretyping | |
| parent | 9ce6802ea563437b15e45198f4d8d0f716a576bb (diff) | |
Conversion of polymorphic inductive types was incomplete in VM and native.
Was showing up when comparing e.g. prod Type Type with prod Type Type (!) with
a polymorphic prod.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/reductionops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index bb1bc7d2ea..0714c93b4f 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1282,7 +1282,7 @@ let sigma_compare_sorts env pb s0 s1 sigma = | Reduction.CONV -> Evd.set_eq_sort env sigma s0 s1 | Reduction.CUMUL -> Evd.set_leq_sort env sigma s0 s1 -let sigma_compare_instances flex i0 i1 sigma = +let sigma_compare_instances ~flex i0 i1 sigma = try Evd.set_eq_instances ~flex sigma i0 i1 with Evd.UniversesDiffer | Univ.UniverseInconsistency _ -> |