diff options
Diffstat (limited to 'toplevel/recordobj.ml')
| -rwxr-xr-x | toplevel/recordobj.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/recordobj.ml b/toplevel/recordobj.ml index b065d7b57..50f2ef83b 100755 --- a/toplevel/recordobj.ml +++ b/toplevel/recordobj.ml @@ -31,8 +31,8 @@ let typ_lams_of t = let objdef_err ref = errorlabstrm "object_declare" - [< pr_id (Termops.id_of_global (Global.env()) ref); - 'sTR" is not a structure object" >] + (pr_id (Termops.id_of_global (Global.env()) ref) ++ + str" is not a structure object") let objdef_declare ref = let sp = match ref with ConstRef sp -> sp | _ -> objdef_err ref in |