From 34e73d0e0e1e997a05307eaa2fab97d694271efa Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 12 Jun 2003 15:57:48 +0000
Subject: Ajout option translate_syntax pour caractériser l'interprétation du
 traducteur à proprement parler

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

(limited to 'tactics')

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
-- 
cgit v1.2.3