X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicUnification.ml;h=683b3f9df8cdae48a073e85d3e61a69ef81b8386;hb=9c9e979d4c45cf3b1ee01688b2c36fe49190ce98;hp=1ca5bb1dfcc8fba921130b5709d83b8b8c9265d2;hpb=fc4cf455977934bd737c3d6c8675ef7663a6a588;p=helm.git

diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml
index 1ca5bb1df..683b3f9df 100644
--- a/helm/software/components/cic_unification/cicUnification.ml
+++ b/helm/software/components/cic_unification/cicUnification.ml
@@ -132,8 +132,6 @@ let eta_reduce after_beta_expansion after_beta_expansion_body
  with
   WrongShape -> after_beta_expansion
 
-let unif_ty = ref true
-  
 let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
  let module S = CicSubstitution in
  let module C = Cic in
@@ -395,7 +393,6 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
          in
          begin
          let subst,metasenv,ugraph1 = 
-           if not (!unif_ty) then subst,metasenv,ugraph else
            let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv in
            (try
               let tyt,ugraph1 =