the decompose tactic is now working

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

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index 712d8ba589d85f05536f18c9085eb08a58feacad..ae6c7ef50a0b2d3b0b5786dcb7a8668711a70357 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -607,3 +607,13 @@ let saturate_term newmeta metasenv context ty =
    let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
     res,metasenv @ newmetasenv,arguments,lastmeta
 
+let lookup_type metasenv context hyp =
+   let rec aux p = function
+      | Some (Cic.Name name, Cic.Decl t) :: _ when name = hyp -> p, t
+      | Some (Cic.Name name, Cic.Def (_, Some t)) :: _ when name = hyp -> p, t
+      | Some (Cic.Name name, Cic.Def (u, _)) :: tail when name = hyp ->
+         p, fst (CicTypeChecker.type_of_aux' metasenv tail u CicUniv.empty_ugraph)
+      | _ :: tail -> aux (succ p) tail
+      | [] -> raise (ProofEngineTypes.Fail "lookup_type: not premise in the current goal")
+   in
+   aux 1 context