diff options
| author | Matthieu Sozeau | 2014-04-08 15:59:36 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:59 +0200 |
| commit | 4bfb3331804fd191a1d5fb92e99ae17b080f4f7b (patch) | |
| tree | e3c56f70fc23adc16fc365ee1fb60763e393a005 | |
| parent | 4d779fe8ff9c2b81eddb671dc0e60d3743357ce5 (diff) | |
Fix set_leq_sort refusing max(u,Set) <= Set when u is flexible.
| -rw-r--r-- | pretyping/evd.ml | 14 | ||||
| -rw-r--r-- | proofs/clenv.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/2342.v | 2 |
3 files changed, 7 insertions, 11 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index fd6af80b89..652bed5a36 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -373,10 +373,11 @@ let process_universe_constraints univs vars alg local cstrs = match Univ.Universe.level r with | None -> error ("Algebraic universe on the right") | Some rl when Univ.Level.is_small rl -> - (match Univ.Universe.level l with - | Some ll when Univ.LMap.mem ll !vars -> - Univ.enforce_eq l r local - | _ -> raise (Univ.UniverseInconsistency (Univ.Le, l, r, []))) + (if Univ.LSet.for_all (fun l -> + Univ.Level.is_small l || Univ.LMap.mem l !vars) + (Univ.Universe.levels l) then + Univ.enforce_leq l r local + else raise (Univ.UniverseInconsistency (Univ.Le, l, r, []))) | _ -> Univ.enforce_leq l r local else if d == Univ.ULub then match varinfo l, varinfo r with @@ -1112,11 +1113,6 @@ let set_leq_sort evd s1 s2 = | Prop c, Prop c' -> if c == Null && c' == Pos then evd else (raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, []))) - | Type u, Prop _ -> - (match is_sort_variable evd s1 with - | Some (_, false) -> - add_universe_constraints evd (Univ.UniverseConstraints.singleton (u1, Univ.UEq, u2)) - | _ -> raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, []))) | _, _ -> add_universe_constraints evd (Univ.UniverseConstraints.singleton (u1,Univ.ULe,u2)) diff --git a/proofs/clenv.ml b/proofs/clenv.ml index afc8d3b70d..33df4ca978 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -121,7 +121,7 @@ let clenv_environments evd bound t = let mk_clenv_from_env environ sigma n (c,cty) = let evd = create_goal_evar_defs sigma in let (evd,args,concl) = clenv_environments evd n cty in - { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args)); + { templval = mk_freelisted (applist (c,args)); templtyp = mk_freelisted concl; evd = evd; env = environ } diff --git a/test-suite/bugs/closed/2342.v b/test-suite/bugs/closed/2342.v index 094e5466cb..6613b28571 100644 --- a/test-suite/bugs/closed/2342.v +++ b/test-suite/bugs/closed/2342.v @@ -4,5 +4,5 @@ Parameter A : Set. Parameter B : A -> Set. Parameter F : Set -> Prop. -Check (F (forall x, B x)). +Check (F (forall x, B x)). |