diff options
| author | herbelin | 2009-12-12 22:59:29 +0000 |
|---|---|---|
| committer | herbelin | 2009-12-12 22:59:29 +0000 |
| commit | 563d9e1066c7f6f0fb0263101013b015b3faa0bd (patch) | |
| tree | 23d43cbd86999502e1da03bd46ff7d87aafa0ccc /interp | |
| parent | aba4b1924f562d861ab2cf7ec75c507f0efe0d1f (diff) | |
Fixed incorrect computation of possible guard in presence of `{ ... } contexts.
Also removed used of local_binders_length and local_assums_length
which are now incorrect due to the possible presence of `{ ... } contexts.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12579 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |