| C.Variable _ -> raise ReferenceToVariable
| C.CurrentProof (_,_,_,_,params) -> raise RferenceToCurrentProof
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
- )
- in
- fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l''
+ ) in
+ fix_according_to_type
+ constant_type (C.Const(uri,exp_named_subst)) l''
+(*
+ 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 *)
| _ -> C.Appl l' )
| C.Const (uri,exp_named_subst) ->
let exp_named_subst' =
| Cic.InductiveDefinition (l,_,n) -> l,n
) in
let (_,_,_,constructors) = List.nth inductive_types tyno in
- prerr_endline ("QUI");
let constructor_types =
let rec clean_up t =
function
+
+
+
+
+
+