diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index e74405549c..17b947ebd0 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -642,8 +642,9 @@ and intern_tactic ist tac = (snd (intern_tactic_seq ist tac) : glob_tactic_expr) and intern_tactic_seq ist = function (* Traducteur v7->v8 *) | TacAtom (_,TacReduce (Unfold [_,Ident (_,id)],_)) - when string_of_id id = "INZ" -> ist.ltacvars, TacId - + when string_of_id id = "INZ" & !Options.translate_syntax + -> ist.ltacvars, TacId + (* Fin traducteur v7->v8 *) | TacAtom (loc,t) -> let lf = ref ist.ltacvars in |