From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 29 Mar 2006 12:18:56 +0000 (+0000)
Subject: removed unif_ty ref
X-Git-Tag: make_still_working~7449
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=54a261cf8956b1c9576fe24a86d37db336de8a64;p=helm.git

removed unif_ty ref
---

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 = 
diff --git a/helm/software/components/cic_unification/cicUnification.mli b/helm/software/components/cic_unification/cicUnification.mli
index 5d0b34e28..e1a6c2899 100644
--- 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