From 17ec7a0c875014e5322f6098dcd2014072cde9d8 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 18 Oct 2016 14:23:23 +0200
Subject: Improve the documentation of eauto.

Improve the description of what auto/eauto do.
These two tactics rely on the simple version of apply/eapply.
Since this simple version is available to the end user,
it is better to mention it. See also the confusion that such
description can create in the thread "Understanding auto" on Coq-Club.
---
 doc/refman/RefMan-tac.tex | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 5eb8cedd95..fc6d9c143c 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3513,8 +3513,8 @@ intact. \texttt{auto} and \texttt{trivial} never fail.
 
 This tactic generalizes {\tt auto}. While {\tt auto} does not try
 resolution hints which would leave existential variables in the goal,
-{\tt eauto} does try them (informally speaking, it uses {\tt eapply}
-where {\tt auto} uses {\tt apply}).
+{\tt eauto} does try them (informally speaking, it uses
+{\tt simple eapply} where {\tt auto} uses {\tt simple apply}).
 As a consequence, {\tt eauto} can solve such a goal:
 
 \begin{coq_eval}
@@ -3529,8 +3529,7 @@ eauto.
 Abort.
 \end{coq_eval}
 
-Note that {\tt ex\_intro} should be declared as an
-hint.
+Note that {\tt ex\_intro} should be declared as a hint.
 
 \SeeAlso Section~\ref{Hints-databases}
 
-- 
cgit v1.2.3


From 6791a37b4e4ba9be829959b419e37a96e2eb5b84 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 18 Oct 2016 16:51:21 +0200
Subject: Document info_auto.

Now that this tactic has been fixed (commit 58d1381),
it needed to get documented.
---
 doc/refman/RefMan-tac.tex | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index fc6d9c143c..dccd6f5907 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3490,6 +3490,12 @@ hints of the database named {\tt core}.
 
   This combines the effects of the {\tt using} and {\tt with} options.
 
+\item {\tt info\_auto}
+
+  Behaves like {\tt auto} but shows the tactics it uses to solve the goal.
+  This variant is very useful for getting a better understanding of automation,
+  or to know what lemmas/assumptions were used.
+
 \item {\tt trivial}\tacindex{trivial}
 
   This tactic is a restriction of {\tt auto} that is not recursive and
-- 
cgit v1.2.3


From 8d77523f8883fae56a8a338060bb2a52b0fd566c Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 18 Oct 2016 16:56:58 +0200
Subject: Extending the doc with a general summary of auto variants.

This way of giving the summary avoids redundancy as much as possible.
It is helpful for the auto-completion of Company-Coq of @cpitclaudel.
---
 doc/refman/RefMan-tac.tex | 30 +++++++++++++++++++++++++-----
 1 file changed, 25 insertions(+), 5 deletions(-)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index dccd6f5907..49a5b7983a 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3472,7 +3472,7 @@ hints of the database named {\tt core}.
   Uses the hint databases $\ident_1$ \dots\ $\ident_n$ in addition to
   the database {\tt core}. See Section~\ref{Hints-databases} for the
   list of pre-defined databases and the way to create or extend a
-  database.  This option can be combined with the previous one.
+  database.
 
 \item {\tt auto with *}
 
@@ -3486,16 +3486,18 @@ hints of the database named {\tt core}.
   $lemma_i$ is an inductive type, it is the collection of its
   constructors which is added as hints.
 
-\item \texttt{auto using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$ with \ident$_1$ {\ldots} \ident$_n$
-
-  This combines the effects of the {\tt using} and {\tt with} options.
-
 \item {\tt info\_auto}
 
   Behaves like {\tt auto} but shows the tactics it uses to solve the goal.
   This variant is very useful for getting a better understanding of automation,
   or to know what lemmas/assumptions were used.
 
+\item {\tt \zeroone{info\_}auto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$
+  {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with}
+  \ident$_1$ {\ldots} \ident$_n$}
+
+  This is the most general form, combining the various options.
+
 \item {\tt trivial}\tacindex{trivial}
 
   This tactic is a restriction of {\tt auto} that is not recursive and
@@ -3506,6 +3508,14 @@ hints of the database named {\tt core}.
 
 \item \texttt{trivial with *}
 
+\item \texttt{trivial using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$
+
+\item {\tt info\_trivial}
+
+\item {\tt \zeroone{info\_}trivial} \zeroone{{\tt using} \nterm{lemma}$_1$
+  {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with}
+  \ident$_1$ {\ldots} \ident$_n$}
+
 \end{Variants}
 
 \Rem {\tt auto} either solves completely the goal or else leaves it
@@ -3537,6 +3547,16 @@ Abort.
 
 Note that {\tt ex\_intro} should be declared as a hint.
 
+\begin{Variants}
+
+\item {\tt \zeroone{info\_}eauto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$
+  {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with}
+  \ident$_1$ {\ldots} \ident$_n$}
+
+  The various options for eauto are the same as for auto.
+
+\end{Variants}
+
 \SeeAlso Section~\ref{Hints-databases}
 
 \subsection{\tt autounfold with \ident$_1$ \mbox{\dots} \ident$_n$}
-- 
cgit v1.2.3


From 5be957316c23db6366aefc246d1d24480aa2f1ea Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 19 Oct 2016 14:18:52 +0200
Subject: Making the doc of auto hints more precise.

The doc of auto hints now mention again that sometimes a hint
will be used with simple apply and sometimes it will be used
with exact.
It does not try to be fully precise in that we don't
necessarily want to document the behaviors of auto that
we might like to change.
See also the discussion on commit 9227d6e.
---
 doc/refman/RefMan-tac.tex | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 49a5b7983a..263766b272 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3709,11 +3709,12 @@ The {\hintdef} is one of the following expressions:
   the number of subgoals generated by {\tt simple apply {\term}}.
 %{\tt auto} actually uses a slightly modified variant of {\tt simple apply} with use_metas_eagerly_in_conv_on_closed_terms set to false
 
-  % Is it really needed?
-  %% In case the inferred type of \term\ does not start with a product
-  %% the tactic added in the hint list is {\tt exact {\term}}. In case
-  %% this type can however be reduced to a type starting with a product,
-  %% the tactic {\tt apply {\term}} is also stored in the hints list.
+  In case the inferred type of \term\ does not start with a product
+  the tactic added in the hint list is {\tt exact {\term}}.
+% Actually, a slightly restricted version is used (no conversion on the head symbol)
+  In case
+  this type can however be reduced to a type starting with a product,
+  the tactic {\tt simple apply {\term}} is also stored in the hints list.
 
   If the inferred type of \term\ contains a dependent quantification
   on a variable which occurs only in the premisses of the type and not
-- 
cgit v1.2.3


From 3a507c03c91efe67afa9f2dd51bf77c7af6df0f5 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 19 Oct 2016 18:09:36 +0200
Subject: Documenting Hint Resolve -> and <- variants.

These variants are from 8.3 but were never documented except in CHANGES.
---
 doc/refman/RefMan-tac.tex | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 263766b272..11de4f35e0 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3744,6 +3744,17 @@ The {\hintdef} is one of the following expressions:
 
     Adds each \texttt{Resolve} {\term$_i$}.
 
+  \item {\tt Resolve -> \term}
+
+    Adds the left-to-right implication of an equivalence as a hint
+    (informally the hint will be used as {\tt apply <- \term},
+    although as mentionned before, the tactic actually used is
+    a restricted version of apply).
+
+  \item {\tt Resolve <- \term}
+
+    Adds the right-to-left implication of an equivalence as a hint.
+
   \end{Variants}
 
 \item \texttt{Immediate {\term}}
-- 
cgit v1.2.3


From 1d769e02b3baba54246c942fe116abaf850892db Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 24 Oct 2016 11:44:24 +0200
Subject: Fix 6d5fe92e to #5150 (missing dependencies in test suite) was a bit
 too strong.

New fix. A bit less consistent with the spirit of this Makefile as we
list prerequisite files explicitly, but avoid to redo subsystems at
each call to "make" as with previous fix.

Other solutions from experts are welcome.
---
 test-suite/Makefile | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 8500ef1b3d..491b16960e 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -84,6 +84,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
 #######################################################################
@@ -221,7 +224,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)"; \
@@ -253,7 +256,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,$<); \
@@ -267,7 +270,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,$<); \
@@ -289,7 +292,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out prerequisite
 	  rm $$tmpoutput; \
 	} > "$@"
 
-$(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,$<); \
@@ -307,7 +310,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,$<); \
@@ -338,7 +341,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,$<); \
-- 
cgit v1.2.3


From 5f1dd4c401110d6b10350c847805c6923fa09de5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 24 Oct 2016 17:04:41 +0200
Subject: Fixing #3479 (parsing of "{" and "}" when a keyword starts with "{"
 or "}").

---
 parsing/lexer.ml4              | 6 ++++++
 test-suite/success/Notations.v | 6 ++++++
 2 files changed, 12 insertions(+)

diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 5d96873f31..db6816a704 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -535,6 +535,12 @@ let rec next_token = parser bp
             next_token s
         | [< t = process_chars bp c >] -> comment_stop bp; t >] ->
       t
+  | [< ' ('{' | '}' as c); s >] ep ->
+      let t,new_between_com =
+        if !between_com then (KEYWORD (String.make 1 c), (bp, ep)), true
+        else process_chars bp c s,false
+      in
+      comment_stop bp; between_com := new_between_com; t
   | [< s >] ->
       match lookup_utf8 s with
         | Utf8Token (Unicode.Letter, n) ->
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 2f7c62972a..511b60b4bb 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -110,3 +110,9 @@ Goal True -> True. intros H. exact H. Qed.
 
 (* Check absence of collision on ".." in nested notations with ".." *)
 Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)).
+
+(* 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.
-- 
cgit v1.2.3


From 0be88deef5e9ace1323cf8adc474bf2e4ada9153 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 24 Oct 2016 17:16:00 +0200
Subject: Fixing a location bug with "?" and "$".

---
 parsing/lexer.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index db6816a704..cfea8793ac 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -495,7 +495,7 @@ let rec next_token = parser bp
   | [< '' ' | '\t' | '\n' |'\r' as c; s >] ->
       comm_loc bp; push_char c; next_token s
   | [< ''$' as c; t = parse_after_special c bp >] ep ->
-      comment_stop bp; (t, (ep, bp))
+      comment_stop bp; (t, (bp, ep))
   | [< ''.' as c; t = parse_after_special c bp; s >] ep ->
       comment_stop bp;
       (* We enforce that "." should either be part of a larger keyword,
@@ -514,7 +514,7 @@ let rec next_token = parser bp
       in
       comment_stop bp; between_com := new_between_com; t
   | [< ''?'; s >] ep ->
-      let t = parse_after_qmark bp s in comment_stop bp; (t, (ep, bp))
+      let t = parse_after_qmark bp s in comment_stop bp; (t, (bp, ep))
   | [< ' ('a'..'z' | 'A'..'Z' | '_' as c);
        len = ident_tail (store 0 c); s >] ep ->
       let id = get_buff len in
-- 
cgit v1.2.3