From c982d8e516e990f19e9f5bdb4967a526095810f2 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 6 Feb 2004 10:25:04 +0000 Subject: [PATCH] Bug MutCase fixed: now the type of the constructor only eats the left params. --- helm/ocaml/cic_omdoc/eta_fixing.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml index c37911014..49a68d1d0 100644 --- a/helm/ocaml/cic_omdoc/eta_fixing.ml +++ b/helm/ocaml/cic_omdoc/eta_fixing.ml @@ -270,7 +270,15 @@ let eta_fix metasenv t = 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 -- 2.39.2