diff options
| -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 _| |