Merge branch 'v8.5' into v8.6

+ a few improvements on 5f1dd4c40 (lexing of { and }).

3 files changed, 24 insertions, 10 deletions

diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 8a8e41956..79771f3f6 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -573,7 +573,7 @@ let rec next_token loc = parser bp
       comment_stop bp; between_commands := new_between_commands; t
   | [< ''?'; s >] ep ->
       let t = parse_after_qmark loc bp s in
-      comment_stop bp; (t, set_loc_pos loc ep bp)
+      comment_stop bp; (t, set_loc_pos loc bp ep)
   | [< ' ('a'..'z' | 'A'..'Z' | '_' as c);
        len = ident_tail loc (store 0 c); s >] ep ->
       let id = get_buff len in
@@ -593,6 +593,12 @@ let rec next_token loc = parser bp
             let loc = comment loc bp s in next_token loc s
         | [< t = process_chars loc bp c >] -> comment_stop bp; t >] ->
       t
+  | [< ' ('{' | '}' as c); s >] ep ->
+      let t,new_between_commands =
+        if !between_commands then (KEYWORD (String.make 1 c), set_loc_pos loc bp ep), true
+        else process_chars loc bp c s, false
+      in
+      comment_stop bp; between_commands := new_between_commands; t
   | [< s >] ->
       match lookup_utf8 loc s with
         | Utf8Token (Unicode.Letter, n) ->
@@ -603,9 +609,7 @@ let rec next_token loc = parser bp
             (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep
         | AsciiChar | Utf8Token ((Unicode.Symbol | Unicode.IdentPart | Unicode.Unknown), _) ->
             let t = process_chars loc bp (Stream.next s) s in
-            let new_between_commands = match t with
-              (KEYWORD ("{"|"}"),_) -> !between_commands | _ -> false in
-            comment_stop bp; between_commands := new_between_commands; t
+            comment_stop bp; t
         | EmptyStream ->
             comment_stop bp; (EOI, set_loc_pos loc bp (bp+1))
 
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 10eb2df39..6a18c45df 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -88,6 +88,9 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
 # All subsystems
 SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk
 
+PREREQUISITELOG = prerequisite/admit.v.log			\
+  prerequisite/make_local.v.log prerequisite/make_notation.v.log
+
 #######################################################################
 # Phony targets
 #######################################################################
@@ -226,7 +229,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
 	  fi; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v prerequisite
+$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \
@@ -257,7 +260,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v
 	  fi; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v prerequisite
+$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -271,7 +274,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v prerequisite
 	  fi; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out prerequisite
+$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -330,7 +333,7 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
 	  rm $$tmpexpected; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v prerequisite
+$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -348,7 +351,7 @@ $(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v prerequisite
 # the .v file with exactly two digits after the dot. The reference for
 # time is a 6120 bogomips cpu.
 ifneq (,$(bogomips))
-$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v prerequisite
+$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -379,7 +382,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v prerequisite
 endif
 
 # Ideal-features tests
-$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v prerequisite
+$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 30abd961b..666c91257 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -115,3 +115,10 @@ Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)).
 Require Import Coq.Vectors.VectorDef.
 Import VectorNotations.
 Goal True. idtac; []. (* important for test: no space here *) constructor. Qed.
+
+(* Check parsing of { and } is not affected by notations #3479 *)
+Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10).
+Goal True.
+{{ exact I. }}
+Qed.
+Check |- {{ 0 }} 0.