Plugs back external tactics.

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

1 files changed, 5 insertions, 5 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 38f3398d5..238edd659 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1227,7 +1227,9 @@ and interp_tacarg ist arg =
         interp_tacarg ist a >>== fun a_interp ->
         acc >>== fun acc -> (Proofview.Goal.return (a_interp::acc))
       end la ((Proofview.Goal.return [])) >>== fun la_interp ->
-      tac_of_old (fun gl -> interp_external loc ist { gl with sigma=project gl } com req la_interp)
+      Proofview.Goal.enterl begin fun gl ->
+        interp_external loc ist gl com req la_interp
+      end
   | TacFreshId l ->
       Proofview.Goal.enterl begin fun gl ->
       let id = Tacmach.New.of_old (fun gl -> pf_interp_fresh_id ist gl l) gl in
@@ -1497,12 +1499,10 @@ and apply_hyps_context ist env lz mt lctxt lgmatch mhyps hyps =
   apply_hyps_context_rec lctxt lgmatch hyps mhyps
   end
 
-and interp_external loc ist gl com req la = assert false
-(* arnaud: todo
-  let f ch = extern_request ch req gl la in
+and interp_external loc ist gl com req la =
+  let f ch = Tacmach.New.of_old (fun gl -> extern_request ch req gl la) gl in
   let g ch = internalise_tacarg ch in
   interp_tacarg ist (System.connect f g com)
-*)
 
 (* Interprets extended tactic generic arguments *)
 and interp_genarg ist gl x =