From 979451471e37a76ce15e45f7b174a49cbb73f9ae Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 25 Aug 1999 14:12:43 +0000
Subject: modules Instantiate, Constant et Inductive

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@22 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/generic.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/generic.ml')

diff --git a/kernel/generic.ml b/kernel/generic.ml
index 9adc53ce68..3e33dca7b7 100644
--- a/kernel/generic.ml
+++ b/kernel/generic.ml
@@ -570,6 +570,9 @@ let rel_list n m =
   in 
   reln [] 1
 
+let rec count_dlam = function
+  | DLAM (_,c) -> 1 + (count_dlam c)
+  | _ -> 0
 
 (* Hash-consing *)
 let comp_term t1 t2 =
-- 
cgit v1.2.3