From b2d2129ff0c807678a0225270f8ccd92dbd3705e Mon Sep 17 00:00:00 2001
From: delahaye
Date: Mon, 18 Mar 2002 17:51:13 +0000
Subject: Rétablissement de look_for_interp

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2540 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tacinterp.ml | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index f84266a1de..2343351c4e 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
-- 
cgit v1.2.3