From 68a3ac0e08c42c7ecc2834e0627c9ed42dc84d05 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 2 Sep 2005 09:58:02 +0000 Subject: [PATCH] Serious bug fixed previously introduced by me in the kernel fixed: in some cases an application with no arguments was created. --- helm/ocaml/cic_proof_checking/cicTypeChecker.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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) -> -- 2.39.2