diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/topconstr.ml | 10 | ||||
| -rw-r--r-- | interp/topconstr.mli | 6 |
2 files changed, 0 insertions, 16 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 3d2e3fde0d..e594f9a9df 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -693,16 +693,6 @@ type constr_pattern_expr = constr_expr let default_binder_kind = Default Explicit -let rec local_binders_length = function - | [] -> 0 - | LocalRawDef _::bl -> 1 + local_binders_length bl - | LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl - -let rec local_assums_length = function - | [] -> 0 - | LocalRawDef _::bl -> local_binders_length bl - | LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl - let names_of_local_assums bl = List.flatten (List.map (function LocalRawAssum(l,_,_)->l|_->[]) bl) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 36f8cfad39..6e3951b2fa 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -216,12 +216,6 @@ val mkCProdN : loc -> local_binder list -> constr_expr -> constr_expr (* For binders parsing *) -(* Includes let binders *) -val local_binders_length : local_binder list -> int - -(* Excludes let binders *) -val local_assums_length : local_binder list -> int - (* With let binders *) val names_of_local_binders : local_binder list -> name located list |