diff options
| author | herbelin | 2008-05-08 23:29:40 +0000 |
|---|---|---|
| committer | herbelin | 2008-05-08 23:29:40 +0000 |
| commit | 9f4236db9a4b8f50fff19f55a009c28ef0c9cdbe (patch) | |
| tree | faa506628d5b91c6cb5d00d2e90a4b507cf54ce1 /contrib/interface/xlate.ml | |
| parent | 672ba13a7287dc2b6d5a28960deacc4966d364aa (diff) | |
Autre oubli de la révision 10904
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10909 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface/xlate.ml')
| -rw-r--r-- | contrib/interface/xlate.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 20bb3a4a1f..9f7491d5f4 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -2191,7 +2191,6 @@ let rec xlate_vernac = List.map reference_to_ct_ID l)) | VernacImport(_, []) -> assert false | VernacProof t -> CT_proof_with(xlate_tactic t) - | VernacVar _ -> xlate_error "Grammar vernac obsolete" | (VernacGlobalCheck _|VernacPrintOption _| VernacMemOption (_, _)|VernacRemoveOption (_, _) | VernacBack _ | VernacBacktrack _ |VernacBackTo _|VernacRestoreState _| VernacWriteState _| |