diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/topconstr.ml | 5 | ||||
| -rw-r--r-- | interp/topconstr.mli | 3 |
2 files changed, 8 insertions, 0 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 855fcb329f..57f2c6a892 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -554,6 +554,11 @@ let rec local_binders_length = function | 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 e06a482159..e1d35bb274 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -159,6 +159,9 @@ val prod_constr_expr : constr_expr -> local_binder list -> constr_expr (* Includes let binders *) val local_binders_length : local_binder list -> int +(* Excludes let binders *) +val local_assums_length : local_binder list -> int + (* Does not take let binders into account *) val names_of_local_assums : local_binder list -> name located list |