From 426cf657448e91ddce1485cb827ebf3879e3db3b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 7 Jul 2006 16:30:34 +0000
Subject: 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
---
 interp/topconstr.ml  | 5 +++++
 interp/topconstr.mli | 3 +++
 2 files changed, 8 insertions(+)

(limited to 'interp')

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
 
-- 
cgit v1.2.3