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 aacace7b5614e975d718cb7bf8750683f205b7f2..282383d7853ae344ecbb75e09ca45e9d586202c7 100644 (file)
--- 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 =