Less use of the list-based interface for goal-bound tactics.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17002 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 14 insertions, 16 deletions

diff --git a/tactics/elim.ml b/tactics/elim.ml
index de4c58371..9c1107beb 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -87,7 +87,7 @@ let up_to_delta = ref false (* true *)
 
 let general_decompose recognizer c =
   Proofview.Goal.enter begin fun gl ->
-  let type_of = Tacmach.New.pf_apply Typing.type_of gl in
+  let type_of = Tacmach.New.pf_type_of gl in
   try (* type_of can raise exceptions *)
   let typc = type_of c in
   Tacticals.New.tclTHENS (Proofview.V82.tactic (cut typc))
@@ -99,24 +99,22 @@ let general_decompose recognizer c =
   with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end
 
-let head_in =
-  Goal.env >- fun env ->
-  Goal.defs >- fun sigma ->
-  Goal.return begin
-    fun indl t ->
-      try
-        let ity,_ =
-          if !up_to_delta
-          then find_mrectype env sigma t
-          else extract_mrectype t
-        in List.mem ity indl
-      with Not_found -> false
-  end
+let head_in indl t gl =
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
+  try
+    let ity,_ =
+      if !up_to_delta
+      then find_mrectype env sigma t
+      else extract_mrectype t
+    in List.mem ity indl
+  with Not_found -> false
 
 let decompose_these c l =
+  Proofview.Goal.enter begin fun gl ->
   let indl = (*List.map inductive_of*) l in
-  Proofview.Goal.lift head_in >>= fun head_in ->
-  general_decompose (fun (_,t) -> head_in indl t) c
+  general_decompose (fun (_,t) -> head_in indl t gl) c
+  end
 
 let decompose_nonrec c =
   general_decompose