From 5d460ffd88d9883dee251dc6b7f1faa6cc7f1a75 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 15 Dec 2002 12:15:00 +0000
Subject: Ajout "Locate Notation"

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

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 2ceb5789c6..0d3739636e 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1535,6 +1535,7 @@ let xlate_vernac =
   | VernacLocate(LocateTerm id) -> CT_locate(reference_to_ct_ID id)
   | VernacLocate(LocateLibrary id) -> CT_locate_lib(reference_to_ct_ID id)
   | VernacLocate(LocateFile s) -> CT_locate_file(CT_string s)
+  | VernacLocate(LocateNotation _) -> xlate_error "TODO: Locate Notation"
   | (VernacGlobalCheck _|VernacPrintOption _|
      VernacMemOption (_, _)|VernacRemoveOption (_, _)|VernacAddOption (_, _)|
      VernacSetOption (_, _)|VernacUnsetOption _|
-- 
cgit v1.2.3