| 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 =
let elim_of ~sort uri typeno =
counter := ~-1;
- let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in
+ let (obj, univ) = (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) in
match obj with
| Cic.InductiveDefinition (indTypes, params, leftno, _) ->
let (name, inductive, ty, constructors) =
*)
let (computed_type, ugraph) =
try
- CicTypeChecker.type_of_aux' [] [] eliminator_body CicUniv.empty_ugraph
+ CicTypeChecker.type_of_aux' [] [] eliminator_body
+ CicUniv.oblivion_ugraph
with CicTypeChecker.TypeCheckerFailure msg ->
raise (Elim_failure (lazy (sprintf
"type checker failure while type checking:\n%s\nerror:\n%s"