diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-17 23:53:15 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-17 23:53:15 +0000 |
| commit | 0910fb8a82bd927f1e65854516cac7300e56de96 (patch) | |
| tree | ab2d18934489bc174bc3155508776161d87e65a1 /contrib/interface | |
| parent | 9a5c5db122becb63c5b72a967ef141bdd3fb5319 (diff) | |
Locate Module
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6325 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/xlate.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index b0a0f4977..182440d64 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -2053,6 +2053,7 @@ let rec xlate_vernac = | VernacReserve([], _) -> assert false | VernacLocate(LocateTerm id) -> CT_locate(reference_to_ct_ID id) | VernacLocate(LocateLibrary id) -> CT_locate_lib(reference_to_ct_ID id) + | VernacLocate(LocateModule _) -> xlate_error "TODO: Locate Module" | VernacLocate(LocateFile s) -> CT_locate_file(CT_string s) | VernacLocate(LocateNotation s) -> CT_locate_notation(CT_string s) | VernacTime(v) -> CT_time(xlate_vernac v) |