diff options
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 |