removed unif_ty ref

[helm.git] / components / cic_unification / cicUnification.ml

diff --git a/components/cic_unification/cicUnification.ml b/components/cic_unification/cicUnification.ml
index 1ca5bb1dfcc8fba921130b5709d83b8b8c9265d2..683b3f9df8cdae48a073e85d3e61a69ef81b8386 100644 (file)
--- 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 =