diff options
| author | Gaetan Gilbert | 2017-04-22 12:55:46 +0200 |
|---|---|---|
| committer | Gaetan Gilbert | 2017-04-27 21:42:01 +0200 |
| commit | b20d52da0d040fe37bb75b0b739ad7686f9af127 (patch) | |
| tree | 6d8612f3a528dab9dd44add1ba26323fd8a41ce7 /interp | |
| parent | 4e84e83911c1cf7613a35b921b1e68e097f84b5a (diff) | |
Warning 29: non escaped end of line may be non portable
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 389880c5c5..3f99a3c7c0 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -855,9 +855,9 @@ let intern_qualid loc qid intern env lvar us args = | Some _, GApp (loc, GRef (loc', ref, None), arg) -> GApp (loc, GRef (loc', ref, us), arg) | Some _, _ -> - user_err ~loc (str "Notation " ++ pr_qualid qid ++ - str " cannot have a universe instance, its expanded head - does not start with a reference") + user_err ~loc (str "Notation " ++ pr_qualid qid + ++ str " cannot have a universe instance," + ++ str " its expanded head does not start with a reference") in c, projapp, args2 |