From a0df6a89bd29e7e058d0734c93549789ba477859 Mon Sep 17 00:00:00 2001 From: msozeau Date: Wed, 27 May 2009 17:24:55 +0000 Subject: Populate the sort constraints set correctly during unification. Add a [set_eq_sort_variable] for cases where two universes should be equal, fix [evars_reset_evd] to keep sort constraints and use [whd_sort_var] directly in [whd_evar]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12149 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/evarconv.ml | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 352b76dd9..0d5df1615 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -24,15 +24,22 @@ open Evarutil open Libnames open Evd -let base_sort_conv evd pb s0 s1 = - match (s0,s1) with +let base_sort_conv evd pb s1 s2 = + match (s1,s2) with | (Prop c1, Prop c2) -> if c1 = Null or c2 = Pos then Some evd else None (* Prop <= Set *) - | (Prop c1, Type u) -> if pb = Reduction.CUMUL then Some evd else None + | (Prop c1, Type u) -> + if pb = Reduction.CUMUL then Some evd + else if Evd.is_sort_variable evd s2 then + Some (Evd.define_sort_variable evd s2 s1) + else None | (Type u, Prop c) -> - if Evd.is_sort_variable evd s0 then - Some (Evd.define_sort_variable evd s0 s1) + if Evd.is_sort_variable evd s1 then + Some (Evd.define_sort_variable evd s1 s2) else None - | (Type u1, Type u2) -> Some evd + | (Type u1, Type u2) -> + match pb with + | CONV -> Some (Evd.set_eq_sort_variable evd s1 s2) + | CUMUL -> Some (Evd.set_leq_sort_variable evd s1 s2) let unify_constr_univ evd f cv_pb t1 t2 = match kind_of_term t1, kind_of_term t2 with -- cgit v1.2.3