From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 22 Mar 2005 16:05:54 +0000 (+0000)
Subject: Bug fixed in assumption_tac: a missing (lift n) when a declaration
X-Git-Tag: V_0_6_3_3~2
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0d729d0fb3fd7c798382e16c1f855ce26edad979;p=helm.git

Bug fixed in assumption_tac: a missing (lift n) when a declaration
x : A := t is found in the context.
---

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 38ad2ebfb..be08c4d9e 100644
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -45,7 +45,8 @@ let assumption_tac =
                fst (R.are_convertible context (S.lift n t) ty 
 		       CicUniv.empty_ugraph) -> n
            | (Some (_, C.Def (_,Some ty'))) when
-               fst (R.are_convertible context ty' ty CicUniv.empty_ugraph) -> n
+               fst (R.are_convertible context (S.lift n ty') ty
+                       CicUniv.empty_ugraph) -> n
            | (Some (_, C.Def (t,None))) ->
 	       let ty_t, u = (* TASSI: FIXME *)
 		 CicTypeChecker.type_of_aux' metasenv context (S.lift n t)