diff options
| author | Pierre-Marie Pédrot | 2014-03-01 18:26:26 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-03-01 22:45:39 +0100 |
| commit | 87b510e5b0f363724eae5db9f177f167a3586015 (patch) | |
| tree | 204c7ad1e1ba38945ab58d74e28d8cf67201fe71 /pretyping | |
| parent | bca756eaebf16b6145c65b53629219d2a0a8b1ba (diff) | |
Fixing pervasive comparisons
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/classops.ml | 2 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 2 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 19 |
3 files changed, 19 insertions, 4 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index cd7cd2e0a3..3fe3b3ff29 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -59,7 +59,7 @@ let cl_typ_ord t1 t2 = match t1, t2 with | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2 | CL_CONST c1, CL_CONST c2 -> con_user_ord c1 c2 | CL_IND i1, CL_IND i2 -> ind_user_ord i1 i2 - | _ -> Pervasives.compare t1 t2 + | _ -> Pervasives.compare t1 t2 (** OK *) module ClTyp = struct type t = cl_typ diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index d2c3282dfd..1db4119be4 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -274,7 +274,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) (* else subco () *) else subco () - | x, y when Pervasives.(=) x y -> (** FIXME *) + | x, y when Constr.equal c c' -> if Int.equal (Array.length l) (Array.length l') then let evm = !evdref in let lam_type = Typing.type_of env evm c in diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index dfbe9a0b5d..9f8ba956a9 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -144,6 +144,21 @@ type cs_pattern = | Sort_cs of sorts_family | Default_cs +let eq_obj_typ o1 o2 = + Constr.equal o1.o_DEF o2.o_DEF && + Int.equal o1.o_INJ o2.o_INJ && + List.equal Constr.equal o1.o_TABS o2.o_TABS && + List.equal Constr.equal o1.o_TPARAMS o2.o_TPARAMS && + Int.equal o1.o_NPARAMS o2.o_NPARAMS && + List.equal Constr.equal o1.o_TCOMPS o2.o_TCOMPS + +let eq_cs_pattern p1 p2 = match p1, p2 with +| Const_cs gr1, Const_cs gr2 -> eq_gr gr1 gr2 +| Prod_cs, Prod_cs -> true +| Sort_cs s1, Sort_cs s2 -> Sorts.family_equal s1 s2 +| Default_cs, Default_cs -> true +| _ -> false + let object_table = Summary.ref (Refmap.empty : (cs_pattern * obj_typ) list Refmap.t) ~name:"record-canonical-structs" @@ -221,7 +236,7 @@ let open_canonical_structure i (_,o) = let lo = compute_canonical_projections o in List.iter (fun ((proj,cs_pat),s) -> let l = try Refmap.find proj !object_table with Not_found -> [] in - let ocs = try Some (List.assoc_f Pervasives.(=) cs_pat l) (* FIXME *) + let ocs = try Some (List.assoc_f eq_cs_pattern cs_pat l) with Not_found -> None in match ocs with | None -> object_table := Refmap.add proj ((cs_pat,s)::l) !object_table; @@ -287,7 +302,7 @@ let declare_canonical_structure ref = add_canonical_structure (check_and_decompose_canonical_structure ref) let lookup_canonical_conversion (proj,pat) = - List.assoc_f Pervasives.(=) pat (Refmap.find proj !object_table) (* FIXME *) + List.assoc_f eq_cs_pattern pat (Refmap.find proj !object_table) let is_open_canonical_projection env sigma (c,args) = try |