From e0142811b372f3c32d34f78dc4ff8ca74b02ef63 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 8 Feb 2008 13:44:54 +0000 Subject: [PATCH] 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. --- helm/software/components/library/cicElim.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.39.2