in
C.Meta (n,l')
| C.Sort s -> C.Sort s
- | C.Implicit -> C.Implicit
+ | C.Implicit _ as t -> t
| C.Cast (v,t) -> C.Cast (eta_fix' context v, eta_fix' context t)
| C.Prod (n,s,t) ->
C.Prod
let l' = List.map (eta_fix' context) l
in
(match l' with
+ [] -> assert false
+ | he::tl ->
+ let ty = CicTypeChecker.type_of_aux' metasenv context he in
+ fix_according_to_type ty he tl
+(*
C.Const(uri,exp_named_subst)::l'' ->
let constant_type =
(match CicEnvironment.get_obj uri with
| 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''
- | _ -> C.Appl l' )
+ ) in
+ 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
| 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 =
- CicTypeChecker.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
+
+
+
+
+
+