From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 15 Dec 2008 13:12:28 +0000 (+0000)
Subject: aded some whd, you should be able to declare something like:
X-Git-Tag: make_still_working~4396
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=82f61808091c59aa884eb232b96ee1c655dcb39a;p=helm.git

aded some whd, you should be able to declare something like:
 inductive A : FOO :=
where FOO is defined as a sort (or unfolds to somthing ending with a sort)
---

diff --git a/helm/software/components/library/cicElim.ml b/helm/software/components/library/cicElim.ml
index aacace7b5..282383d78 100644
--- a/helm/software/components/library/cicElim.ml
+++ b/helm/software/components/library/cicElim.ml
@@ -150,14 +150,20 @@ let rec mk_rels consno = function
   | 0 -> []
   | n -> Cic.Rel (n+consno) :: mk_rels consno (n-1)
 
-let rec strip_pi = function
-  | Cic.Prod (_, _, tgt) -> strip_pi tgt
+let rec strip_pi ctx t = 
+  match CicReduction.whd ~delta:true ctx t with
+  | Cic.Prod (n, s, tgt) -> strip_pi (Some (n,Cic.Decl s) :: ctx) tgt
   | t -> t
 
-let rec count_pi = function
-  | Cic.Prod (_, _, tgt) -> count_pi tgt + 1
+let strip_pi t = strip_pi [] t
+
+let rec count_pi ctx t = 
+  match CicReduction.whd ~delta:true ctx t with
+  | Cic.Prod (n, s, tgt) -> count_pi (Some (n,Cic.Decl s)::ctx) tgt + 1
   | t -> 0
 
+let count_pi t = count_pi [] t
+
 let rec type_of_p sort dependent leftno indty = function
   | Cic.Prod (n, src, tgt) when leftno = 0 ->
       let n =