From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 6 Feb 2004 10:25:04 +0000 (+0000)
Subject: Bug MutCase fixed: now the type of the constructor only eats the
X-Git-Tag: V_0_2_3~22
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c982d8e516e990f19e9f5bdb4967a526095810f2;hp=a1f20cae9c37b56f796eafbf7e60dc8f17f8d307;p=helm.git

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