the decompose tactic is now working

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

diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml
index 57c9805139a6a3c4aaa8d9440fda0ba181fd4290..bd2ac9fdeb7d85861cb6f130879ba61ced2d9bd5 100644 (file)
--- a/helm/ocaml/tactics/fwdSimplTactic.ml
+++ b/helm/ocaml/tactics/fwdSimplTactic.ml
@@ -23,9 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(*
+
 module PEH = ProofEngineHelpers 
-*)
 module U  = CicUniv
 module TC = CicTypeChecker 
 module PET = ProofEngineTypes 
@@ -37,7 +36,6 @@ module MI = CicMkImplicit
 module PESR = ProofEngineStructuralRules
 
 let fail_msg0 = "unexported clearbody: invalid argument"
-let fail_msg1 = "fwd: argument is not premise in the current goal"
 let fail_msg2 = "fwd: no applicable simplification"
 
 let error msg = raise (PET.Fail msg)
@@ -106,7 +104,9 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub
       let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
       let lemma = FNG.clean_dummy_dependent_types lemma in
       let metasenv, metas, conts = strip_prods metasenv context ?how_many to_what lemma in      
-      let conclusion =  Cic.Appl (what :: List.rev metas) in
+      let conclusion =  
+         match metas with [] -> what | _ -> Cic.Appl (what :: List.rev metas)
+      in
       let tac = T.thens ~start:(letin_tac conclusion)
                        ~continuations:[clearbody ~index:1]
       in
@@ -122,20 +122,8 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub
 (* fwd **********************************************************************)
 
 let fwd_simpl_tac
-     ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
-     ~dbd hyp
-  =
-   let find_type metasenv context =
-      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 (TC.type_of_aux' metasenv tail u U.empty_ugraph)
-         | _ :: tail -> aux (succ p) tail
-         | [] -> error fail_msg1
-      in
-      aux 1 context
-   in
+     ?(mk_fresh_name_callback = FNG.mk_fresh_name ~subst:[])
+     ~dbd hyp =
    let lapply_tac to_what lemma = 
       lapply_tac ~mk_fresh_name_callback ~how_many:1 ~to_what:[to_what] lemma
    in
@@ -143,7 +131,7 @@ let fwd_simpl_tac
       let (proof, goal) = status in
       let _, metasenv, _, _ = proof in
       let _, context, ty = CicUtil.lookup_meta goal metasenv in
-      let index, major = find_type metasenv context in 
+      let index, major = PEH.lookup_type metasenv context hyp in 
       match MetadataQuery.fwd_simpl ~dbd major with
          | []       -> error fail_msg2
          | uri :: _ ->