X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FfwdSimplTactic.ml;h=10df83c5db482f34dfe30dbd734dee126ca67245;hb=5cfd68a5d9e73edb40e1cfe021a1426354767aa8;hp=ffc90c1cc4948f44c99ee3a1852d20fbaa93aca5;hpb=e31bb143e3a303321e509f415764338849b7e516;p=helm.git

diff --git a/helm/software/components/tactics/fwdSimplTactic.ml b/helm/software/components/tactics/fwdSimplTactic.ml
index ffc90c1cc..10df83c5d 100644
--- a/helm/software/components/tactics/fwdSimplTactic.ml
+++ b/helm/software/components/tactics/fwdSimplTactic.ml
@@ -35,6 +35,7 @@ module T = Tacticals
 module FNG = FreshNamesGenerator
 module MI = CicMkImplicit
 module PESR = ProofEngineStructuralRules
+module HEL = HExtlib
 
 let fail_msg0 = "unexported clearbody: invalid argument"
 let fail_msg2 = "fwd: no applicable simplification"
@@ -46,7 +47,7 @@ let error msg = raise (PET.Fail (lazy msg))
 let id_tac = 
    let id_tac (proof,goal) = 
       try
-         let _, metasenv, _, _ = proof in
+         let _, metasenv, _subst, _, _, _ = proof in
          let _, _, _ = CicUtil.lookup_meta goal metasenv in
          (proof,[goal])
       with CicUtil.Meta_not_found _ -> (proof, [])
@@ -61,7 +62,7 @@ let clearbody ~index =
    in
    let clearbody status =
       let (proof, goal) = status in
-      let _, metasenv, _, _ = proof in
+      let _, metasenv, _subst, _, _, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       PET.apply_tactic (PESR.clearbody ~hyp:(find_name index context)) status
    in
@@ -102,15 +103,15 @@ let get_clearables context terms =
       | Cic.Appl (Cic.Rel i :: _) -> PEH.get_name context i
       | _                         -> None
    in
-   PEH.list_rev_map_filter aux terms 
+   HEL.list_rev_map_filter aux terms 
 
 let lapply_tac_aux ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) 
                (* ?(substs = []) *) ?how_many ?(to_what = []) what =
    let letin_tac term = PT.letin_tac ~mk_fresh_name_callback term in   
    let lapply_tac (proof, goal) =
-      let xuri, metasenv, u, t = proof in
+      let xuri, metasenv, _subst, u, t, attrs = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
-      let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
+      let lemma, _ = TC.type_of_aux' metasenv context what U.oblivion_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 =  
@@ -120,7 +121,7 @@ let lapply_tac_aux ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name
 	 T.then_ ~start:(letin_tac conclusion) 
                  ~continuation:(clearbody ~index:1)	 
       in
-      let proof = (xuri, metasenv, u, t) in
+      let proof = (xuri, metasenv, _subst, u, t, attrs) in
       let aux (proof, goals) (tac, goal) = 
          let proof, new_goals = PET.apply_tactic tac (proof, goal) in
 	 proof, goals @ new_goals
@@ -133,7 +134,7 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub
                (* ?(substs = []) *) ?(linear = false) ?how_many ?(to_what = []) what =
    let lapply_tac status =
       let proof, goal = status in
-      let _, metasenv, _, _ = proof in
+      let _, metasenv, _subst, _, _, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let lapply = lapply_tac_aux ~mk_fresh_name_callback ?how_many ~to_what what in
       let tac =  
@@ -158,7 +159,7 @@ let fwd_simpl_tac
    in
    let fwd_simpl_tac status =
       let (proof, goal) = status in
-      let _, metasenv, _, _ = proof in
+      let _, metasenv, _subst, _, _, _ = proof in
       let _, context, ty = CicUtil.lookup_meta goal metasenv in
       let index, major = PEH.lookup_type metasenv context hyp in 
       match FwdQueries.fwd_simpl ~dbd major with