diff options
| author | herbelin | 2003-01-15 15:30:23 +0000 |
|---|---|---|
| committer | herbelin | 2003-01-15 15:30:23 +0000 |
| commit | a6ce286c10edf79a57c69acffc67fcd254b88d36 (patch) | |
| tree | d16b26cf263eab04afa9362a63721d389ad48129 /contrib/interface | |
| parent | a70a5e4bddec01dc2dfa18180f3fd5f795618922 (diff) | |
Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à une sorte
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3497 85f007b7-540e-0410-9357-904b9bb8a0f7
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 *) |