X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FvariousTactics.ml;h=c1006032471a7d6fffc86959dcedca987c4a05bf;hb=423f3f23abfe6d5906818c26ab92d3703714057d;hp=38ad2ebfbee4f1f76030e7fafaace0263a186b0c;hpb=31851952e1cc2db59168c5fd6f6093d9bc37ea86;p=helm.git

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 38ad2ebfb..c10060324 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) 
@@ -112,4 +113,12 @@ let generalize_tac
   PET.mk_tactic (generalize_tac mk_fresh_name_callback terms)
 ;;
 
+let set_goal n =
+  ProofEngineTypes.mk_tactic
+    (fun (proof, goal) ->
+       let (_, metasenv, _, _) = proof in
+       if CicUtil.exists_meta n metasenv then
+         (proof, [n])
+       else
+         raise (ProofEngineTypes.Fail ("no such meta: " ^ string_of_int n)))