X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=3b8e4ad221646ba6f0e949eb1250e2ba04e477bb;hb=ed9af5a10b66343f817a1f9eac3add29e4b2baae;hp=768255a1493db265c087ecad4355b934d8354b19;hpb=d3af4c289c9870337a141a0ffa98f9e01439d806;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 768255a14..3b8e4ad22 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -232,17 +232,6 @@ let apply_subst_gen ~appl_fun subst term =
 ;;
 
 let apply_subst =
-(* CSC: old code that never performs beta reduction
-  let appl_fun um_aux he tl =
-    let tl' = List.map um_aux tl in
-      begin
-       match um_aux he with
-          Cic.Appl l -> Cic.Appl (l@tl')
-        | he' -> Cic.Appl (he'::tl')
-      end
-  in
-  apply_subst_gen ~appl_fun
-*)
   let appl_fun um_aux he tl =
     let tl' = List.map um_aux tl in
     let t' =
@@ -252,18 +241,7 @@ let apply_subst =
     in
      begin
       match he with
-         Cic.Meta (m,_) ->
-          let rec beta_reduce =
-           function
-              (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
-                let he'' = CicSubstitution.subst he' t in
-                 if tl' = [] then
-                  he''
-                 else
-                  beta_reduce (Cic.Appl(he''::tl'))
-            | t -> t
-          in
-           beta_reduce t'
+         Cic.Meta (m,_) -> CicReduction.head_beta_reduce t'
        | _ -> t'
      end
   in