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 38ad2ebfbee4f1f76030e7fafaace0263a186b0c..be08c4d9e9b69bf5114ba1f4c62d6384ea8a312e 100644 (file)
--- 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)