From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 2 Sep 2005 09:58:02 +0000 (+0000)
Subject: Serious bug fixed previously introduced by me in the kernel fixed: in some cases
X-Git-Tag: V_0_1_2_1~123
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=68a3ac0e08c42c7ecc2834e0627c9ed42dc84d05;p=helm.git

Serious bug fixed previously introduced by me in the kernel fixed: in some cases
an application with no arguments was created.
---

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 43805cf8b..6d26f8848 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1766,12 +1766,12 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
           if not branches_ok then
            raise
             (TypeCheckerFailure "Case analysys: wrong branch type");
-          let arguments =
+          let arguments' =
            if not need_dummy then outtype::arguments@[term]
            else outtype::arguments in
           let outtype =
-           if arguments = [] then outtype
-           else CicReduction.head_beta_reduce (C.Appl arguments)
+           if need_dummy && arguments = [] then outtype
+           else CicReduction.head_beta_reduce (C.Appl arguments')
           in
            outtype,ugraph5
    | C.Fix (i,fl) ->