| 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
if noparams = 0 then
List.map (fun (_,t) -> t) constructors
else
- let term_type =
- TypeInference.type_of_aux' metasenv context term in
+ let term_type =
+ CicTypeChecker.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 rec first_n n l =
+ if n = 0 then []
+ else
+ (match l with
+ a::tl -> a::(first_n (n-1) tl)
+ | _ -> assert false) in
+ List.map
+ (fun (_,t) ->
+ clean_up t (first_n noparams params)) constructors
| _ -> prerr_endline ("QUA"); assert false) in
let patterns2 =
List.map2 fix_lambdas_wrt_type
+
+
+
+
+
+