X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicUnification.ml;h=683b3f9df8cdae48a073e85d3e61a69ef81b8386;hb=7f21c77a04c282e789dfbedf202fe90e15a7fde2;hp=1ca5bb1dfcc8fba921130b5709d83b8b8c9265d2;hpb=801f0eb3eabe1cbcd66d6a3f52c24eb8f1189611;p=helm.git

diff --git a/components/cic_unification/cicUnification.ml b/components/cic_unification/cicUnification.ml
index 1ca5bb1df..683b3f9df 100644
--- a/components/cic_unification/cicUnification.ml
+++ b/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 =