From 0d729d0fb3fd7c798382e16c1f855ce26edad979 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 22 Mar 2005 16:05:54 +0000 Subject: [PATCH] Bug fixed in assumption_tac: a missing (lift n) when a declaration x : A := t is found in the context. --- helm/ocaml/tactics/variousTactics.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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) -- 2.39.2