diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-06-14 09:15:38 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-06-14 09:15:38 +0000 |
| commit | 3f1769a8002addec9f53969affd6b4cee1ccbbea (patch) | |
| tree | cab9b33832658113f646ebc38d78cd0bb2c83de3 /contrib/interface/xlate.ml | |
| parent | 8ddd9ba6efcd32a13b4517a4e80c5fc035a951a8 (diff) | |
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
Diffstat (limited to 'contrib/interface/xlate.ml')
| -rw-r--r-- | contrib/interface/xlate.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 54f22c646..c6baa0ecf 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 _) |