Asts generalized: a lot of tactics where restricted to identifiers in place

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

diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml
index 7981ac8753727962ad64f8443c13385a642b6e77..98125f5e738d447986bdb88f74aed4825ef646e6 100644 (file)
--- a/helm/ocaml/tactics/fwdSimplTactic.ml
+++ b/helm/ocaml/tactics/fwdSimplTactic.ml
@@ -30,24 +30,13 @@ module U  = CicUniv
 module S = CicSubstitution
 module PT = PrimitiveTactics
 
-(*
-let module R = CicReduction
-*)
-
-let fail_msg0 = "not a declaration of the current context"
 let fail_msg1 = "no applicable simplification"
 
 let error msg = raise (PET.Fail msg)
 
-let rec declaration name = function 
-   | []                                           -> error fail_msg0
-   | Some (hyp, Cic.Decl ty) :: _ when hyp = name -> ty
-   | _ :: tail                                    -> declaration name tail 
-
 (* lapply *******************************************************************)
 
-let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
-               ?(substs = []) what =
+let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) what =
    let rec strip_dependent_prods metasenv context ss = function
       | Cic.Prod (name, t1, t2) as t -> 
         if TC.does_not_occur context 0 1 t2 then metasenv, ss, t else 
@@ -74,12 +63,14 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub
 
 (* fwd **********************************************************************)
 
-let fwd_simpl_tac ~hyp ~dbd =
+let fwd_simpl_tac ~term ~dbd =
    let fwd_simpl_tac status =
       let (proof, goal) = status in
       let _,metasenv,_,_ = proof in
       let _,context,ty = CicUtil.lookup_meta goal metasenv in
-      let major = declaration hyp context in 
+      let major,_ =
+       CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
+      in 
       match  MetadataQuery.fwd_simpl ~dbd major with
          | []       -> error fail_msg1
          | uri :: _ -> prerr_endline (UriManager.string_of_uri uri); (proof, [])