diff options
| -rw-r--r-- | library/universes.ml | 2 | ||||
| -rw-r--r-- | pretyping/evd.ml | 12 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 6 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 8 | ||||
| -rw-r--r-- | test-suite/success/unicode_utf8.v | 2 | ||||
| -rw-r--r-- | theories/MSets/MSetGenTree.v | 2 |
6 files changed, 21 insertions, 11 deletions
diff --git a/library/universes.ml b/library/universes.ml index 7d1908d1f..f1c9c85a2 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -645,7 +645,7 @@ let universes_of_constr c = match kind_of_term c with | Const (_, u) | Ind (_, u) | Construct (_, u) -> LSet.union (Instance.levels u) s - | Sort u -> + | Sort u when not (Sorts.is_small u) -> let u = univ_of_sort u in LSet.union (Universe.levels u) s | _ -> fold_constr aux s c diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 166bab4b8..fd6af80b8 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -372,7 +372,12 @@ let process_universe_constraints univs vars alg local cstrs = else match Univ.Universe.level r with | None -> error ("Algebraic universe on the right") - | Some _ -> Univ.enforce_leq l r local + | 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, []))) + | _ -> Univ.enforce_leq l r local else if d == Univ.ULub then match varinfo l, varinfo r with | (Inr (l, true, _), Inr (r, _, _)) @@ -1107,6 +1112,11 @@ 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/pretyping/retyping.ml b/pretyping/retyping.ml index c967bc7ad..0c2bad5c6 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -69,12 +69,12 @@ let rec subst_type env sigma typ = function (* [sort_of_atomic_type] computes ft[args] which has to be a sort *) let sort_of_atomic_type env sigma ft args = - let rec concl_of_arity env ar args = + let rec concl_of_arity env n ar args = match kind_of_term (whd_betadeltaiota env sigma ar), args with - | Prod (na, t, b), h::l -> concl_of_arity (push_rel (na,Some h,t) env) b l + | Prod (na, t, b), h::l -> concl_of_arity (push_rel (na,Some (lift n h),t) env) (n + 1) b l | Sort s, [] -> s | _ -> retype_error NotASort - in concl_of_arity env ft (Array.to_list args) + in concl_of_arity env 0 ft (Array.to_list args) let type_of_var env id = try let (_,_,ty) = lookup_named id env in ty diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index c6c404992..dc9cc471c 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -633,12 +633,12 @@ let unify_eqn env (sigma, cstrs) hypinfo by t = and ty2 = Typing.type_of env'.env env'.evd c2 in if convertible env env'.evd ty1 ty2 then - (if occur_meta_or_existential prf then + (* (if occur_meta_or_existential prf then *) (hypinfo := refresh_hypinfo env env'.evd !hypinfo; env'.evd, prf, c1, c2, car, rel) - else (** Evars have been solved, we can go back to the initial evd, - but keep the potential refinement of existing evars. *) - env'.evd, prf, c1, c2, car, rel) + (* else (\** Evars have been solved, we can go back to the initial evd, *) + (* but keep the potential refinement of existing evars. *\) *) + (* env'.evd, prf, c1, c2, car, rel) *) else raise Reduction.NotConvertible in let evars = evd', Evar.Set.empty in diff --git a/test-suite/success/unicode_utf8.v b/test-suite/success/unicode_utf8.v index bfddd8468..50a65310d 100644 --- a/test-suite/success/unicode_utf8.v +++ b/test-suite/success/unicode_utf8.v @@ -11,7 +11,7 @@ Parameter π : ℝ. (** Check indices *) Definition test_indices : nat -> nat := fun x₁ => x₁. -Definition π₂ := snd. +Definition π₂ := @snd. (** More unicode in identifiers *) Definition αβ_áà_אב := 0. diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 6164e6e93..2ec125427 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -962,7 +962,7 @@ Proof. firstorder. Qed. Lemma eq_Leq : forall s s', eq s s' <-> L.eq (elements s) (elements s'). Proof. unfold eq, Equal, L.eq; intros. - do 2 setoid_rewrite elements_spec1. (*FIXME due to regression in rewrite *) + setoid_rewrite elements_spec1. firstorder. Qed. |