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 43805cf8b24f1dc692277d2ea738db580ad446b4..6d26f88488914291f2513c395fa2880863598b73 100644 (file)
--- 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) ->