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
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