let t2 =
match t' with
C.Appl l ->
- C.LetIn (C.Name "w",t',C.Appl ((C.Rel 1)::(mk_rels no_sources 1)))
+ C.LetIn (C.Name "w",t',assert false,
+ C.Appl ((C.Rel 1)::(mk_rels no_sources 1)))
| _ -> C.Appl (t'::(mk_rels no_sources 0)) in
List.fold_right
(fun source t -> C.Lambda (C.Name "y",CicReduction.whd [] source,t)) sources t2
(* prerr_endline ("******* too many args: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); *)
C.LetIn
(C.Name "H",
- C.Appl res, C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
+ C.Appl res,
+ assert false,
+ C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
else
let name,source,target =
(match ty with
| C.Lambda (n,s,t) ->
C.Lambda
(n, eta_fix' context s, eta_fix' ((Some (n,(C.Decl s)))::context) t)
- | C.LetIn (n,s,t) ->
+ | C.LetIn (n,s,ty,t) ->
C.LetIn
- (n,eta_fix' context s,eta_fix' ((Some (n,(C.Def (s,None))))::context) t)
+ (n,eta_fix' context s,eta_fix' context ty,
+ eta_fix' ((Some (n,(C.Def (s,ty))))::context) t)
| C.Appl [] -> assert false
| C.Appl (he::tl) ->
let tl' = List.map (eta_fix' context) tl in
let ty,_ =
CicTypeChecker.type_of_aux' metasenv context he
- CicUniv.empty_ugraph
+ CicUniv.oblivion_ugraph
in
fix_according_to_type ty (eta_fix' context he) tl'
(*
let term' = eta_fix' context term in
let patterns' = List.map (eta_fix' context) patterns in
let inductive_types,noparams =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
(match o with
Cic.Constant _ -> assert false
| Cic.Variable _ -> assert false
else
let term_type,_ =
CicTypeChecker.type_of_aux' metasenv context term
- CicUniv.empty_ugraph
+ CicUniv.oblivion_ugraph
in
(match term_type with
C.Appl (hd::params) ->
(fun newsubst (uri,t) ->
let t' = eta_fix' context t in
let ty =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
match o with
Cic.Variable (_,_,ty,_,_) ->
CicSubstitution.subst_vars newsubst ty