From b20d52da0d040fe37bb75b0b739ad7686f9af127 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Sat, 22 Apr 2017 12:55:46 +0200
Subject: Warning 29: non escaped end of line may be non portable

---
 interp/constrintern.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'interp')

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
 
-- 
cgit v1.2.3