From f8ae76ca7965e176094496bf17dd77bff1acae10 Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 4 Mar 2009 19:47:42 +0000
Subject: illegal tactic application was having Ltac interpreter loop

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11963 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index ac65d3a52a..9df3ba4ec0 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1846,7 +1846,11 @@ and interp_tacarg ist gl = function
 (* Interprets an application node *)
 and interp_app loc ist gl fv largs =
   match fv with
-    | VFun(trace,olfun,var,body) ->
+      (* if var=[] this means that evaluation of body has been delayed
+         by val_interp, so it is not a tactic that expects arguments.
+         Otherwise Ltac goes into an infinite loop (val_interp puts
+         a VFun back on body, and then interp_app is called again...) *)
+    | VFun(trace,olfun,(_::_ as var),body) ->
       let (newlfun,lvar,lval)=head_with_value (var,largs) in
       if lvar=[] then
 	let v = 
-- 
cgit v1.2.3