Bug MutCase fixed: now the type of the constructor only eats the

left params.

diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml
index c379110145b522a87d441d5f322f9cf69c7d7d21..49a68d1d0d23c9504f61c53248064d8410ee9c98 100644 (file)
--- 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