diff options
Diffstat (limited to 'kernel/mod_typing.ml')
| -rw-r--r-- | kernel/mod_typing.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index e8c831f705..e14e7c9008 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -34,13 +34,6 @@ let rec list_split_assoc k rev_before = function | (k',b)::after when k=k' -> rev_before,b,after | h::tail -> list_split_assoc k (h::rev_before) tail -let rec list_fold_map2 f e = function - | [] -> (e,[],[]) - | h::t -> - let e',h1',h2' = f e h in - let e'',t1',t2' = list_fold_map2 f e' t in - e'',h1'::t1',h2'::t2' - let discr_resolver env mtb = match mtb.typ_expr with SEBstruct _ -> |