* (Head) beta reduction functions factorized

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index a9593c67fb617782815a6631fcc3cfa18c9b5f06..76642ee3d51e553309d67b6294e4a475761b4613 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -559,7 +559,9 @@ and type_of_aux' metasenv context t ugraph =
                        candidate outtype ugraph5
                    in
                      C.MutCase (uri, i, outtype, term', pl'),
-                       (Cic.Appl (outtype::right_args@[term'])),
+                      CicReduction.head_beta_reduce
+                       (CicMetaSubst.apply_subst subst
+                        (Cic.Appl (outtype::right_args@[term']))),
                      subst,metasenv,ugraph)
            | _ ->    (* easy case *)
              let _,_, subst, metasenv,ugraph5 =
@@ -584,8 +586,9 @@ and type_of_aux' metasenv context t ugraph =
                  (subst,metasenv,ugraph5) outtypeinstances 
              in
                C.MutCase (uri, i, outtype, term', pl'),
-                 CicReduction.whd ~subst       context 
-                   (C.Appl(outtype::right_args@[term])),
+                 CicReduction.head_beta_reduce
+                  (CicMetaSubst.apply_subst subst
+                   (C.Appl(outtype::right_args@[term]))),
                  subst,metasenv,ugraph6)
        | C.Fix (i,fl) ->
            let fl_ty',subst,metasenv,types,ugraph1 =