diff options
| author | herbelin | 2006-07-07 16:30:34 +0000 |
|---|---|---|
| committer | herbelin | 2006-07-07 16:30:34 +0000 |
| commit | 426cf657448e91ddce1485cb827ebf3879e3db3b (patch) | |
| tree | a011502bddd7b4d6b6f860c3d04e7bc5b6ad1086 /interp | |
| parent | 027b617df7880d211f4060d015abb00ab8616e8a (diff) | |
Correction bug 1172 + correction en passant de la taille des paramètres de famille
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9032 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |