From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 25 Oct 2005 15:48:18 +0000 (+0000)
Subject: fixed lapply on new tinycals semantic
X-Git-Tag: V_0_7_2_3~189
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dbe5d5ee749b3d5d36c91f96b73d7554967fc8cd;p=helm.git

fixed lapply on new tinycals semantic
removed expand_implicits from elim
---

diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml
index 16510a7cd..a5c7878c7 100644
--- a/helm/ocaml/tactics/fwdSimplTactic.ml
+++ b/helm/ocaml/tactics/fwdSimplTactic.ml
@@ -107,8 +107,8 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub
       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]
+      let tac = T.then_ ~start:(letin_tac conclusion) 
+        ~continuation:(clearbody ~index:1)
       in
       let proof = (xuri, metasenv, u, t) in
       let aux (proof, goals) (tac, goal) = 
@@ -137,7 +137,7 @@ let fwd_simpl_tac
          | uri :: _ -> 
 	    Printf.eprintf "fwd: %s\n" (UriManager.string_of_uri uri); flush stderr;
 	    let start = lapply_tac (Cic.Rel index) (Cic.Const (uri, [])) in  
-            let tac = T.thens ~start ~continuations:[PESR.clear hyp] in
+            let tac = T.then_ ~start ~continuation:(PESR.clear hyp) in
             PET.apply_tactic tac status
    in
    PET.mk_tactic fwd_simpl_tac
diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index d26221d39..96ff130c5 100644
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -517,10 +517,8 @@ let elim_tac ~term =
           in
            C.Appl (eliminator_ref :: make_tl term (args_no - 1))
          in
-          let metasenv', term_to_refine' =
-           CicMkImplicit.expand_implicits metasenv' [] context term_to_refine in
           let refined_term,_,metasenv'',_ = 
-           CicRefine.type_of_aux' metasenv' context term_to_refine' 
+           CicRefine.type_of_aux' metasenv' context term_to_refine
              CicUniv.empty_ugraph
           in
            let new_goals =