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 | |
| 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
| -rw-r--r-- | contrib/interface/xlate.ml | 6 | ||||
| -rw-r--r-- | test-suite/success/Record.v | 3 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 9 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 2 |
4 files changed, 16 insertions, 4 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 *) diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v new file mode 100644 index 0000000000..f3a13634df --- /dev/null +++ b/test-suite/success/Record.v @@ -0,0 +1,3 @@ +(* Nijmegen expects redefinition of sorts *) +Definition CProp := Prop. +Record test : CProp := { n:nat }. diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 5bba0c630b..62a08d0492 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -444,7 +444,14 @@ let vernac_record struc binders sort nameopt cfs = let const = match nameopt with | None -> add_prefix "Build_" (snd struc) | Some id -> id in - let s = interp_sort sort in + let sigma = Evd.empty in + let env = Global.env() in + let s = interp_constr sigma env sort in + let s = Reductionops.whd_betadeltaiota env sigma s in + let s = match kind_of_term s with + | Sort s -> s + | _ -> user_err_loc + (constr_loc sort,"definition_structure", str "Sort expected") in Record.definition_structure (struc,binders,cfs,const,s) (* Sections *) diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 51d080faf9..8980a7eaa2 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -183,7 +183,7 @@ type vernac_expr = (* Gallina extensions *) | VernacRecord of identifier with_coercion * simple_binder list - * sort_expr * identifier option * local_decl_expr with_coercion list + * constr_expr * identifier option * local_decl_expr with_coercion list | VernacBeginSection of identifier | VernacEndSegment of identifier | VernacRequire of |