From 2788c86e6a3c089aa7450a7768f8444470e35901 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 9 Mar 2016 17:11:46 +0100
Subject: Fix test-suite file coq-prog-args

They were not parsed correctly with a newline in the middle.
---
 test-suite/bugs/closed/4533.v | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v
index 217ea8a4c7..ae17fb145d 100644
--- a/test-suite/bugs/closed/4533.v
+++ b/test-suite/bugs/closed/4533.v
@@ -1,5 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." 
-"Top" "-top" "bug_lex_wrong_rewrite_02") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_lex_wrong_rewrite_02") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 1125 lines to 
 346 lines, then from 360 lines to 346 lines, then from 822 lines to 271 lines, 
 then from 285 lines to 271 lines *)
@@ -12,6 +11,7 @@ Tactic Notation "admit" := case proof_admitted.
 Require Coq.Init.Datatypes.
 Import Coq.Init.Notations.
 Global Set Universe Polymorphism.
+Global Set Primitive Projections.
 Notation "A -> B" := (forall (_ : A), B) : type_scope.
 Module Export Datatypes.
   Set Implicit Arguments.
@@ -202,6 +202,7 @@ Module Type Preserves_Fibers (Os : ReflectiveSubuniverses).
   Module Export Os_Theory := ReflectiveSubuniverses_Theory Os.
 End Preserves_Fibers.
 
+Opaque eissect.
 Module Lex_Reflective_Subuniverses
        (Os : ReflectiveSubuniverses) (Opf : Preserves_Fibers Os).
   Import Opf.
@@ -221,4 +222,5 @@ v = _) r,
     match goal with
     | [ |- p2 @ p0 @ p1 @ eissect (to O A) (g x) = r ] => idtac "good"
     | [ |- ?G ] => fail 1 "bad" G
-    end.
\ No newline at end of file
+    end.
+    Fail rewrite concat_p_pp.
\ No newline at end of file
-- 
cgit v1.2.3