From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 8 Feb 2008 13:44:54 +0000 (+0000)
Subject: Bug fixed in generation of elimination principles of inductive types having
X-Git-Tag: make_still_working~5623
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e0142811b372f3c32d34f78dc4ff8ca74b02ef63;p=helm.git

Bug fixed in generation of elimination principles of inductive types having
at least one constructor of type (A -> i) -> i that was not the last
constructor.
---

diff --git a/helm/software/components/library/cicElim.ml b/helm/software/components/library/cicElim.ml
index c994a9c53..22bece033 100644
--- a/helm/software/components/library/cicElim.ml
+++ b/helm/software/components/library/cicElim.ml
@@ -217,7 +217,7 @@ let rec branch (uri, typeno) insource paramsno t fix head args =
       if insource then
         (match args with
         | [arg] -> Cic.Appl (fix :: args)
-        | _ -> Cic.Appl (head :: [Cic.Appl args]))
+        | _ -> Cic.Appl (fix :: [Cic.Appl args]))
       else
         (match args with
         | [] -> head