From 3f1769a8002addec9f53969affd6b4cee1ccbbea Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 14 Jun 2003 09:15:38 +0000
Subject: Ajout option Local à Hint, Hints et HintDestruct

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

(limited to 'contrib/interface')

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 54f22c6460..c6baa0ecf9 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1361,7 +1361,8 @@ let xlate_vernac =
 	  (fst::rest) -> CT_formula_ne_list(fst,rest)
 	| _ -> assert false in
       CT_hintrewrite(ct_orient, f_ne_list, CT_ident base, xlate_tactic t)
-  | VernacHints (dbnames,h) ->
+  | VernacHints (local,dbnames,h) ->
+      (* TODO: locality flag *)
       let dblist = CT_id_list(List.map (fun x -> CT_ident x) dbnames) in
       (match h with
 	| HintsResolve [Some id_name, c] -> (* = Old HintResolve *)
@@ -1668,7 +1669,7 @@ let xlate_vernac =
   | (VernacGlobalCheck _|VernacPrintOption _|
      VernacMemOption (_, _)|VernacRemoveOption (_, _)|VernacAddOption (_, _)|
      VernacSetOption (_, _)|VernacUnsetOption _|
-     VernacHintDestruct (_, _, _, _, _)|VernacBack _|VernacRestoreState _|
+     VernacHintDestruct (_, _, _, _, _, _)|VernacBack _|VernacRestoreState _|
      VernacWriteState _|VernacSolveExistential (_, _)|VernacCanonical _|
      VernacImport (_, _)|VernacExactProof _|VernacDistfix _|
      VernacTacticGrammar _|VernacVar _|VernacTime _|VernacProof _)
-- 
cgit v1.2.3