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 | |
| 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
| -rw-r--r-- | contrib/interface/depends.ml | 3 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 1 |
2 files changed, 2 insertions, 2 deletions
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml index d2b94b39ea..be4f9c091a 100644 --- a/contrib/interface/depends.ml +++ b/contrib/interface/depends.ml @@ -94,7 +94,8 @@ let rec depends_of_hole_kind hk acc = match hk with | Evd.QuestionMark _ | Evd.CasesType | Evd.InternalHole - | Evd.GoalEvar -> acc + | Evd.GoalEvar + | Evd.ImpossibleCase -> acc let depends_of_'a_cast_type depends_of_'a act acc = match act with | CastConv (ck, a) -> depends_of_'a a acc 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 _| |