diff options
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/xlate.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 9ddf7268a3..1ed4dd9b0c 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1378,7 +1378,7 @@ let xlate_vernac = | (*Record from tactics/Record.v *) VernacRecord - ((add_coercion, s), binders, c1, rec_constructor_or_none, field_list) -> + ((add_coercion, s), binders, CSort (_,c1), rec_constructor_or_none, field_list) -> let record_constructor = xlate_ident_opt rec_constructor_or_none in CT_record ((if add_coercion then CT_coercion_atm else @@ -1386,6 +1386,8 @@ let xlate_vernac = xlate_ident s, cvt_vernac_binders binders, xlate_sort c1, record_constructor, build_record_field_list field_list) + | VernacRecord _ -> xlate_error "TODO: Record in a defined sort" + (* TODO | (*Inversions from tactics/Inv.v *) "MakeSemiInversionLemmaFromHyp", @@ -1543,7 +1545,7 @@ let xlate_vernac = VernacHintDestruct (_, _, _, _, _)|VernacBack _|VernacRestoreState _| VernacWriteState _|VernacSolveExistential (_, _)|VernacCanonical _| VernacImport (_, _)|VernacExactProof _|VernacDistfix (_, _, _, _, _)| - VernacTacticGrammar _|VernacVar _|VernacTime _) + VernacTacticGrammar _|VernacVar _|VernacTime _|VernacProof _) -> xlate_error "TODO: vernac" (* Modules and Module Types *) |