From 3eaa27e3e4a5e022c3b72cf1617564a332082029 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 25 Sep 2006 02:03:26 +0000
Subject:  Permet a un unfold de recevoir ses occurences a travers une variable
 Ltac.  P.ex:     Tactic Notation "test" integer(i) := unfold plus at i  Ou
 meme:     Tactic Notation "test" ne_integer_list(i) := unfold plus at i 
 (voir commit 9159 d'Hugo).

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

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a12c09ec8c..b6ad913f6e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1307,7 +1307,7 @@ let pf_interp_type ist gl =
 
 (* Interprets a reduction expression *)
 let interp_unfold ist env (l,qid) =
-  (l,interp_evaluable ist env qid)
+  (interp_int_or_var_list ist l,interp_evaluable ist env qid)
 
 let interp_flag ist env red =
   { red with rConst = List.map (interp_evaluable ist env) red.rConst }
-- 
cgit v1.2.3