From ba5f2cc720dd8fbb74214cfd99d63fb7330ffce3 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 20 May 2009 15:35:12 +0000 Subject: [PATCH] Removed a silly type check --- .../software/components/tactics/paramodulation/indexing.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) 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 = -- 2.39.2