removed unif_ty ref

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

diff --git a/helm/software/components/cic_unification/cicUnification.mli b/helm/software/components/cic_unification/cicUnification.mli
index 5d0b34e28c1c3c8da76d11e2978ef5304ac19dd5..e1a6c2899e446026f352c91b33ad4e6c53f13f73 100644 (file)
--- a/helm/software/components/cic_unification/cicUnification.mli
+++ b/helm/software/components/cic_unification/cicUnification.mli
@@ -56,4 +56,3 @@ val fo_unif_subst :
     Cic.term -> Cic.term -> CicUniv.universe_graph ->
       Cic.substitution * Cic.metasenv * CicUniv.universe_graph
 
-    val unif_ty : bool ref