X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=7a67c8248e4e5d72d7986166cd5ec9f5401213cc;hb=b8ac0d11d5cd4083838a3848fce68683a518b54a;hp=5e2eaba0046fca7544454395852a995acc258ca6;hpb=5530db2f72548a8c579ae5f9868cbd38290eb065;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 5e2eaba00..7a67c8248 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -50,29 +50,6 @@ let type_of_aux' metasenv subst context term ugraph =
 let exists_a_meta l = 
   List.exists (function Cic.Meta _ -> true | _ -> false) l
 
-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
-(* 
-let rec deref subst =
-  let snd (_,a,_) = a in
-  function
-      Cic.Meta(n,l) as t -> 
-        (try 
-           deref subst
-             (CicSubstitution.subst_meta 
-                l (snd (CicUtil.lookup_subst n subst))) 
-         with 
-           CicUtil.Subst_not_found _ -> t)
-    | t -> t
-;; *)
-
 let rec deref subst t =
   let snd (_,a,_) = a in
   match t with
@@ -86,10 +63,10 @@ let rec deref subst t =
     | Cic.Appl(Cic.Meta(n,l)::args) ->
         (match deref subst (Cic.Meta(n,l)) with
            | Cic.Lambda _ as t -> 
-               deref subst (beta_reduce (Cic.Appl(t::args)))
+               deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
            | r -> Cic.Appl(r::args))
     | Cic.Appl(((Cic.Lambda _) as t)::args) ->
-           deref subst (beta_reduce (Cic.Appl(t::args)))
+           deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
     | t -> t
 ;; 
 
@@ -481,7 +458,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin
               (try 
                  let (_,t,_) = CicUtil.lookup_subst i subst in
                  let lifted = S.subst_meta l t in
-                 let reduced = beta_reduce (Cic.Appl (lifted::args)) in
+                 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
                    fo_unif_subst 
                     test_equality_only 
                      subst context metasenv reduced t2 ugraph
@@ -496,7 +473,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin
               (* (try 
                  let (_,t,_) = CicUtil.lookup_subst i subst in
                  let lifted = S.subst_meta l t in
-                 let reduced = beta_reduce (Cic.Appl (lifted::args)) in
+                 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
                    fo_unif_subst 
                      test_equality_only 
                      subst context metasenv t1 reduced ugraph