Rétablissement de look_for_interp

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

1 files changed, 11 insertions, 3 deletions

diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index f84266a1d..2343351c4 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -563,9 +563,17 @@ let rec val_interp ist ast =
     | Node(loc,s,[]) ->
         VFTactic ([],(interp_atomic s))
     | Node(loc,s,l) ->
-        let fv = val_interp ist (Node(loc,"PRIMTACTIC",[Node(loc,s,[])]))
-        and largs = List.map (val_interp ist) l in
-        app_interp ist fv largs ast
+        (try
+          ((look_for_interp s) ist ast)
+        with
+           Not_found ->
+             if l = [] then
+               VFTactic ([],(interp_atomic s))
+             else
+               let fv = val_interp ist
+                          (Node(loc,"PRIMTACTIC",[Node(loc,s,[])]))
+               and largs = List.map (val_interp ist) l in
+               app_interp ist fv largs ast)
     | Dynamic(_,t) ->
       let tg = (tag t) in
       if tg = "tactic" then