diff options
| author | Pierre-Marie Pédrot | 2014-06-17 14:26:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-06-17 15:44:38 +0200 |
| commit | 90d64647d3fd5dbf5c337944dc0038f0b19b8a51 (patch) | |
| tree | b33528c72730ec541a75e3d0baaead6789f4dcb9 /pretyping/recordops.ml | |
| parent | d412844753ef25f4431c209f47b97b9fa498297d (diff) | |
Removing dead code.
Diffstat (limited to 'pretyping/recordops.ml')
| -rw-r--r-- | pretyping/recordops.ml | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 7250217d68..35ac90de57 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -145,14 +145,6 @@ 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 @@ -241,8 +233,6 @@ let pr_cs_pattern = function | Default_cs -> str "_" | Sort_cs s -> Termops.pr_sort_family s -let pr_pattern (p,c) = pr_cs_pattern p - let open_canonical_structure i (_,o) = if Int.equal i 1 then let lo = compute_canonical_projections o in |