From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 20 May 2009 15:35:12 +0000 (+0000)
Subject: Removed a silly type check
X-Git-Tag: make_still_working~3955
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ba5f2cc720dd8fbb74214cfd99d63fb7330ffce3;p=helm.git

Removed a silly type check
---

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index cf4bcd555..7ff0dfd2c 100644
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -723,10 +723,11 @@ let rec demodulation_equality bag ?from eq_uri env table target =
     let pos, equality = eq_found in
     let (_, proof', 
         (ty, what, other, _), menv',id') = Equality.open_equality equality in
+    (*
     let ty =
-      try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
-      with CicUtil.Meta_not_found _ -> ty
-    in
+      try fst (CicTypeChecker.type_of_aux' menv' context what ugraph)
+      with CicUtil.Meta_not_found _ -> ty 
+    in *)
     let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newterm, newproof =