diff options
| -rw-r--r-- | kernel/indtypes.ml | 3 | ||||
| -rw-r--r-- | kernel/term.ml | 17 | ||||
| -rw-r--r-- | kernel/term.mli | 1 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 2 | ||||
| -rw-r--r-- | pretyping/evd.ml | 6 | ||||
| -rw-r--r-- | pretyping/termops.ml | 2 | ||||
| -rw-r--r-- | toplevel/cerrors.ml | 2 |
7 files changed, 23 insertions, 10 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index ada7c2c512..1aa6e8cda1 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -245,8 +245,7 @@ let typecheck_inductive env mie = begin match kind_of_term c with | Sort (Type u) -> if List.mem (Some u) l then - (** FIXME *) - None :: List.map (function Some v when Pervasives.(=) u v -> None | x -> x) l + None :: List.map (function Some v when Universe.equal u v -> None | x -> x) l else Some u :: l | _ -> diff --git a/kernel/term.ml b/kernel/term.ml index 627919f09f..4eac04f2d3 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -63,6 +63,19 @@ let prop_sort = Prop Null let set_sort = Prop Pos let type1_sort = Type type1_univ +let sorts_ord s1 s2 = + if s1 == s2 then 0 else + match s1, s2 with + | Prop c1, Prop c2 -> + begin match c1, c2 with + | Pos, Pos | Null, Null -> 0 + | Pos, Null -> -1 + | Null, Pos -> 1 + end + | Type u1, Type u2 -> Universe.compare u1 u2 + | Prop _, Type _ -> -1 + | Type _, Prop _ -> 1 + let is_prop_sort = function | Prop Null -> true | _ -> false @@ -566,7 +579,7 @@ let compare_constr f t1 t2 = | Rel n1, Rel n2 -> Int.equal n1 n2 | Meta m1, Meta m2 -> Int.equal m1 m2 | Var id1, Var id2 -> Int.equal (id_ord id1 id2) 0 - | Sort s1, Sort s2 -> Int.equal (Pervasives.compare s1 s2) 0 (** FIXME **) + | Sort s1, Sort s2 -> Int.equal (sorts_ord s1 s2) 0 | Cast (c1,_,_), _ -> f c1 t2 | _, Cast (c2,_,_) -> f t1 c2 | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 && f c1 c2 @@ -612,7 +625,7 @@ let constr_ord_int f t1 t2 = | Rel n1, Rel n2 -> Int.compare n1 n2 | Meta m1, Meta m2 -> Int.compare m1 m2 | Var id1, Var id2 -> id_ord id1 id2 - | Sort s1, Sort s2 -> Pervasives.compare s1 s2 + | Sort s1, Sort s2 -> sorts_ord s1 s2 | Cast (c1,_,_), _ -> f c1 t2 | _, Cast (c2,_,_) -> f t1 c2 | Prod (_,t1,c1), Prod (_,t2,c2) diff --git a/kernel/term.mli b/kernel/term.mli index 85192e1f14..cb48fbbe32 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -21,6 +21,7 @@ val set_sort : sorts val prop_sort : sorts val type1_sort : sorts +val sorts_ord : sorts -> sorts -> int val is_prop_sort : sorts -> bool (** {6 The sorts family of CCI. } *) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index ff4d2837b4..888e4e388b 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -171,7 +171,7 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr) (match s, s' with Prop x, Prop y when x == y -> None | Prop _, Type _ -> None - | Type x, Type y when Pervasives.(=) x y -> None (* false *) (** FIXME **) + | Type x, Type y when Univ.Universe.equal x y -> None (* false *) | _ -> subco ()) | Prod (name, a, b), Prod (name', a', b') -> let name' = Name (Namegen.next_ident_away (id_of_string "x") (Termops.ids_of_context env)) in diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 1c9573ca31..8849f17699 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -514,15 +514,15 @@ let univ_of_sort = function | Prop Null -> Univ.type0m_univ let is_eq_sort s1 s2 = - if Pervasives.(=) s1 s2 then None (* FIXME *) + if Int.equal (sorts_ord s1 s2) 0 then None (* FIXME *) else let u1 = univ_of_sort s1 and u2 = univ_of_sort s2 in - if Pervasives.(=) u1 u2 then None (* FIXME *) + if Univ.Universe.equal u1 u2 then None else Some (u1, u2) let is_univ_var_or_set u = - Univ.is_univ_variable u || Pervasives.(=) u Univ.type0_univ (** FIXME *) + Univ.is_univ_variable u || Univ.is_type0_univ u let set_leq_sort ({evars = (sigma, (us, sm))} as d) s1 s2 = match is_eq_sort s1 s2 with diff --git a/pretyping/termops.ml b/pretyping/termops.ml index c9a6d0b5b6..973f85818c 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -161,7 +161,7 @@ let new_Type_sort () = Type (new_univ ()) let refresh_universes_gen strict t = let modified = ref false in let rec refresh t = match kind_of_term t with - | Sort (Type u) when strict || Pervasives.(<>) u Univ.type0m_univ -> (** FIXME *) + | Sort (Type u) when strict || not (Univ.is_type0m_univ u) -> modified := true; new_Type () | Prod (na,u,v) -> mkProd (na,u,refresh v) | _ -> t in diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 9a9c99c12c..cc455dfeb5 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -77,7 +77,7 @@ let rec process_vernac_interp_error = function str " because" ++ spc() ++ Univ.pr_uni v ++ prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ Univ.pr_uni v) p ++ - (if Pervasives.(=) (snd (List.last p)) u then mt() else (* FIXME *) + (if Univ.Universe.equal (snd (List.last p)) u then mt() else (spc() ++ str "= " ++ Univ.pr_uni u)) in let msg = if !Constrextern.print_universes then |