diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-25 02:03:26 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-25 02:03:26 +0000 |
| commit | 3eaa27e3e4a5e022c3b72cf1617564a332082029 (patch) | |
| tree | 1fde3d79c53b593591abb064144741899ef1b827 | |
| parent | bd07a69adf72e0b888f94a0379691afcf9183975 (diff) | |
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
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index a12c09ec8..b6ad913f6 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 } |