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 /toplevel | |
| 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 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 9 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 2 |
2 files changed, 9 insertions, 2 deletions
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 |