prima implementazione di demodulate, superposition_left e superposition_right

[helm.git] / helm / ocaml / tactics / variousTactics.ml

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 38ad2ebfbee4f1f76030e7fafaace0263a186b0c..c1006032471a7d6fffc86959dcedca987c4a05bf 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) 
@@ -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)))