X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicUntrusted.ml;h=524a00cd35f73cdd4477b8e3191f30ceff7bca31;hb=c301e17392ad24f9d6009be092506dc2313c4427;hp=1d8f6c49e3527ceccacc3a32a2952d7bd2252ec0;hpb=0431f79f14bbf2cdc38c099cacba3a2f71363d7b;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml
index 1d8f6c49e..524a00cd3 100644
--- a/helm/software/components/ng_kernel/nCicUntrusted.ml
+++ b/helm/software/components/ng_kernel/nCicUntrusted.ml
@@ -175,21 +175,23 @@ let rec fire_projection_redex on_args = function
       in
       if pragma <> `Projection || List.length args <= rno then conclude ()
       else
-        (match List.nth args rno with
+        (match List.nth l (rno+1) with
         | C.Appl (C.Const(Ref.Ref(_,Ref.Con _))::_) ->
             let _, _, _, _, fbody = List.nth ifl fno in (* fbody is closed! *)
-            let t = C.Appl (fbody::args) in
+            let t = C.Appl (fbody::List.tl l) in
             (match NCicReduction.head_beta_reduce ~delta:max_int t with
-            | C.Match (_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))::kargs),[pat])->
+             | C.Match (_,_, C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))
+                ::kargs),[pat])->
                   let _,kargs = HExtlib.split_nth leftno kargs in
-        fire_projection_redex false 
-                  (NCicReduction.head_beta_reduce 
-                    ~delta:max_int (C.Appl (pat :: kargs)))
-            | C.Appl(C.Match(_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))::kargs),[pat]) :: args) ->
+                   fire_projection_redex false 
+                    (NCicReduction.head_beta_reduce 
+                      ~delta:max_int (C.Appl (pat :: kargs)))
+            | C.Appl(C.Match(_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))
+               ::kargs),[pat]) :: args) ->
                   let _,kargs = HExtlib.split_nth leftno kargs in
-        fire_projection_redex false 
-                  (NCicReduction.head_beta_reduce 
-                    ~delta:max_int (C.Appl (pat :: kargs @ args)))
+                   fire_projection_redex false 
+                    (NCicReduction.head_beta_reduce 
+                      ~delta:max_int (C.Appl (pat :: kargs @ args)))
             | _ -> conclude ()) 
         | _ -> conclude ())
   | t when on_args -> NCicUtils.map (fun _ x -> x) true fire_projection_redex t