diff options
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/xlate.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index a7288de9a7..de17ca0b67 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -939,6 +939,8 @@ and xlate_tac = CT_injection_eq (xlate_quantified_hypothesis_opt (out_gen (wit_opt rawwit_quant_hyp) idopt)) + | TacExtend (_,"injection_as", [idopt;ipat]) -> + xlate_error "TODO: injection as" | TacFix (idopt, n) -> CT_fixtactic (xlate_ident_opt idopt, CT_int n, CT_fix_tac_list []) | TacMutualFix (id, n, fixtac_list) -> |