exception RferenceToCurrentProof;;
exception ReferenceToInductiveDefinition;;
+let prerr_endline _ = ();;
+
(*
let rec fix_lambdas_wrt_type ty te =
let module C = Cic in
let eta_fix metasenv t =
let rec eta_fix' context t =
- prerr_endline ("entering aux with: term=" ^ CicPp.ppterm t);
- flush stderr ;
+ (* prerr_endline ("entering aux with: term=" ^ CicPp.ppterm t);
+ flush stderr ; *)
let module C = Cic in
let module S = CicSubstitution in
match t with
(n, eta_fix' context s, eta_fix' ((Some (n,(C.Decl s)))::context) t)
| C.LetIn (n,s,t) ->
C.LetIn
- (n, eta_fix' context s, eta_fix' ((Some (n,(C.Def s)))::context) t)
+ (n,eta_fix' context s,eta_fix' ((Some (n,(C.Def (s,None))))::context) t)
| C.Appl l as appl ->
let l' = List.map (eta_fix' context) l
in
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
)
in
- let result = fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l'' in
- if not (CicReduction.are_convertible [] appl result) then
- (prerr_endline ("prima :" ^(CicPp.ppterm appl));
- prerr_endline ("dopo :" ^(CicPp.ppterm result)));
- result
+ fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l''
| _ -> C.Appl l' )
| C.Const (uri,exp_named_subst) ->
let exp_named_subst' =
List.map (fun (_,t) -> t) constructors
else
let term_type =
- CicTypeChecker.type_of_aux' metasenv context term in
+ TypeInference.type_of_aux' metasenv context term in
(match term_type with
C.Appl (hd::params) ->
List.map (fun (_,t) -> clean_up t params) constructors
let patterns2 =
List.map2 fix_lambdas_wrt_type
constructor_types patterns in
- let dopo =
- C.MutCase (uri, tyno, outty',term',patterns2) in
- if not (CicReduction.are_convertible [] prima dopo) then
- (prerr_endline ("prima :" ^(CicPp.ppterm prima));
- prerr_endline ("dopo :" ^(CicPp.ppterm dopo)));
- dopo
+ C.MutCase (uri, tyno, outty',term',patterns2)
| C.Fix (funno, funs) ->
let fun_types =
List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) funs in