diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-05-27 17:24:55 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-05-27 17:24:55 +0000 |
| commit | a0df6a89bd29e7e058d0734c93549789ba477859 (patch) | |
| tree | fabf24b0b87fdd9be9e9cc43abd4ca91801cd637 /pretyping/evarconv.ml | |
| parent | 223c8ca43cdd5a2615b436ef5faa055b182073ac (diff) | |
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
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 19 |
1 files changed, 13 insertions, 6 deletions
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 |