X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcicElim.ml;h=282383d7853ae344ecbb75e09ca45e9d586202c7;hb=8b7ad9b29b3448b72e476ba077e2d0faad86c058;hp=aacace7b5614e975d718cb7bf8750683f205b7f2;hpb=2e2648a9ed26d9b813de8e6a10e2776162565f09;p=helm.git 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 =