* (Head) beta reduction functions factorized

[helm.git] / helm / ocaml / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index fbcf25f91450a4beb8ace412ba213dcfc0fa0d6c..6789c4dff8213acdf53d18aef9b286c0bd46744f 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1766,12 +1766,14 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
           if not branches_ok then
            raise
             (TypeCheckerFailure "Case analysys: wrong branch type");
-          if not need_dummy then
-            (C.Appl ((outtype::arguments)@[term])),ugraph5
-          else if arguments = [] then
-            outtype,ugraph5
-          else
-            (C.Appl (outtype::arguments)),ugraph5
+          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)
+          in
+           outtype,ugraph5
    | C.Fix (i,fl) ->
       let types_times_kl,ugraph1 =
        (* WAS: list rev list map *)
@@ -2117,9 +2119,9 @@ let typecheck uri ugraph =
 
 (** wrappers which instantiate fresh loggers *)
 
-let type_of_aux' ?(subst = []) metasenv context t =
+let type_of_aux' ?(subst = []) metasenv context t ugraph =
   let logger = new CicLogger.logger in
-  type_of_aux' ~logger ~subst metasenv context t
+  type_of_aux' ~logger ~subst metasenv context t ugraph
 
 let typecheck_mutual_inductive_defs uri (itl, uris, indparamsno) =
   let logger = new CicLogger.logger in