From 3be2307af0f1316630b46078fd6b4367c283472d Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 3 Oct 2016 13:57:16 +0200
Subject: Remove if_then_else. Use tryif instead.

if_then_else definition does not account for multi success tactics.
tryif_then_else is a primitive tactical with the expected behavior.
---
 theories/FSets/FSetDecide.v | 19 +++++--------------
 theories/MSets/MSetDecide.v | 19 +++++--------------
 2 files changed, 10 insertions(+), 28 deletions(-)

diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index ad067eb3d8..1db6a71e81 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -357,17 +357,8 @@ the above form:
         | _ => idtac
       end.
 
-    (** [if t then t1 else t2] executes [t] and, if it does not
-        fail, then [t1] will be applied to all subgoals
-        produced.  If [t] fails, then [t2] is executed. *)
-    Tactic Notation
-      "if" tactic(t)
-      "then" tactic(t1)
-      "else" tactic(t2) :=
-      first [ t; first [ t1 | fail 2 ] | t2 ].
-
     Ltac abstract_term t :=
-      if (is_var t) then fail "no need to abstract a variable"
+      tryif (is_var t) then fail "no need to abstract a variable"
       else (let x := fresh "x" in set (x := t) in *; try clearbody x).
 
     Ltac abstract_elements :=
@@ -478,11 +469,11 @@ the above form:
       repeat (
         match goal with
         | H : context [ @Logic.eq ?T ?x ?y ] |- _ =>
-          if (change T with E.t in H) then fail
-          else if (change T with t in H) then fail
+          tryif (change T with E.t in H) then fail
+          else tryif (change T with t in H) then fail
           else clear H
         | H : ?P |- _ =>
-          if prop (FSet_Prop P) holds by
+          tryif prop (FSet_Prop P) holds by
             (auto 100 with FSet_Prop)
           then fail
           else clear H
@@ -747,7 +738,7 @@ the above form:
     | H: (In ?x ?r) -> False |- (E.eq ?y ?x) -> False =>
       contradict H; fsetdec_body
     | H: ?P -> False |- ?Q -> False =>
-      if prop (FSet_elt_Prop P) holds by
+      tryif prop (FSet_elt_Prop P) holds by
         (auto 100 with FSet_Prop)
       then (contradict H; fsetdec_body)
       else fsetdec_body
diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v
index f2555791b2..9c622fd786 100644
--- a/theories/MSets/MSetDecide.v
+++ b/theories/MSets/MSetDecide.v
@@ -357,17 +357,8 @@ the above form:
         | _ => idtac
       end.
 
-    (** [if t then t1 else t2] executes [t] and, if it does not
-        fail, then [t1] will be applied to all subgoals
-        produced.  If [t] fails, then [t2] is executed. *)
-    Tactic Notation
-      "if" tactic(t)
-      "then" tactic(t1)
-      "else" tactic(t2) :=
-      first [ t; first [ t1 | fail 2 ] | t2 ].
-
     Ltac abstract_term t :=
-      if (is_var t) then fail "no need to abstract a variable"
+      tryif (is_var t) then fail "no need to abstract a variable"
       else (let x := fresh "x" in set (x := t) in *; try clearbody x).
 
     Ltac abstract_elements :=
@@ -478,11 +469,11 @@ the above form:
       repeat (
         match goal with
         | H : context [ @Logic.eq ?T ?x ?y ] |- _ =>
-          if (change T with E.t in H) then fail
-          else if (change T with t in H) then fail
+          tryif (change T with E.t in H) then fail
+          else tryif (change T with t in H) then fail
           else clear H
         | H : ?P |- _ =>
-          if prop (MSet_Prop P) holds by
+          tryif prop (MSet_Prop P) holds by
             (auto 100 with MSet_Prop)
           then fail
           else clear H
@@ -747,7 +738,7 @@ the above form:
     | H: (In ?x ?r) -> False |- (E.eq ?y ?x) -> False =>
       contradict H; fsetdec_body
     | H: ?P -> False |- ?Q -> False =>
-      if prop (MSet_elt_Prop P) holds by
+      tryif prop (MSet_elt_Prop P) holds by
         (auto 100 with MSet_Prop)
       then (contradict H; fsetdec_body)
       else fsetdec_body
-- 
cgit v1.2.3


From 25b0a871bde109788492992f1cb417e7e163ffa3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 8 Oct 2016 22:02:12 +0200
Subject: Fixing beautification to file.

---
 toplevel/vernac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 55f3a31a34..bdd834d52f 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -132,7 +132,7 @@ let pr_new_syntax loc ocom =
     | Some com -> Ppvernac.pr_vernac com
     | None -> mt() in
   if !beautify_file then
-    Feedback.msg_notice (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
+    Pp.msg_with !Pp_control.std_ft (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
   else
     Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
   States.unfreeze fs;
-- 
cgit v1.2.3


From 8a8caba36ea6b0fd67e026ee3833d3b5b25af56d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 7 Oct 2016 16:38:26 +0200
Subject: Attaching all extra imperative components of the lexer/parser state
 to the state of parsable streams, so that different lexing/parsing processes
 can be started independently without conflicting.

Note however that these different lexing/parsing processes cannot be
run concurrently as they still work on the same piece of global memory
(i.e. calls to entry_parse should remain atomic). To go further, one
would typically need to be able to functionally pass the lexing state
to each call to the lexer.

Note that currently the beautifier is also running in the context of a
lexer/parser state (for the mapping of location to comments).

In particular, this fixes #5102 (parsing/lexing of bullets depending on
the lexing state which was global).
---
 parsing/cLexer.ml4   | 59 ++++++++++++++++++++--------------------
 parsing/cLexer.mli   |  4 ---
 parsing/compat.ml4   | 76 +++++++++++++++++++++++++++++++++++++++++++---------
 toplevel/coqloop.ml  | 12 +++++----
 toplevel/coqloop.mli |  2 +-
 toplevel/vernac.ml   | 29 +++++++++-----------
 toplevel/vernac.mli  |  4 +--
 7 files changed, 116 insertions(+), 70 deletions(-)

diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index bec891f7f1..777cdc9bf7 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -340,34 +340,35 @@ let comm_loc bp = match !comment_begin with
 | None -> comment_begin := Some bp
 | _ -> ()
 
-let current = Buffer.create 8192
-let between_com = ref true
+let current_comment = Buffer.create 8192
+let between_commands = ref true
 
-type com_state = int option * string * bool
-let restore_com_state (o,s,b) =
+type comments_state = int option * string * bool * ((int * int) * string) list
+let restore_comments_state (o,s,b,c) =
   comment_begin := o;
-  Buffer.clear current; Buffer.add_string current s;
-  between_com := b
-let dflt_com = (None,"",true)
-let com_state () =
-  let s = (!comment_begin, Buffer.contents current, !between_com) in
-  restore_com_state dflt_com; s
+  Buffer.clear current_comment; Buffer.add_string current_comment s;
+  between_commands := b;
+  Pp.comments := c
+let default_comments_state = (None,"",true,[])
+let comments_state () =
+  let s = (!comment_begin, Buffer.contents current_comment, !between_commands, !Pp.comments) in
+  restore_comments_state default_comments_state; s
 
-let real_push_char c = Buffer.add_char current c
+let real_push_char c = Buffer.add_char current_comment c
 
 (* Add a char if it is between two commands, if it is a newline or
    if the last char is not a space itself. *)
 let push_char c =
   if
-    !between_com || List.mem c ['\n';'\r'] ||
+    !between_commands || List.mem c ['\n';'\r'] ||
     (List.mem c [' ';'\t']&&
-     (Int.equal (Buffer.length current) 0 ||
-      not (let s = Buffer.contents current in
+     (Int.equal (Buffer.length current_comment) 0 ||
+      not (let s = Buffer.contents current_comment in
            List.mem s.[String.length s - 1] [' ';'\t';'\n';'\r'])))
   then
     real_push_char c
 
-let push_string s = Buffer.add_string current s
+let push_string s = Buffer.add_string current_comment s
 
 let null_comment s =
   let rec null i =
@@ -375,12 +376,12 @@ let null_comment s =
   null (String.length s - 1)
 
 let comment_stop ep =
-  let current_s = Buffer.contents current in
-  if !Flags.xml_export && Buffer.length current > 0 &&
-    (!between_com || not(null_comment current_s)) then
+  let current_s = Buffer.contents current_comment in
+  if !Flags.xml_export && Buffer.length current_comment > 0 &&
+    (!between_commands || not(null_comment current_s)) then
       Hook.get f_xml_output_comment current_s;
-  (if Flags.do_beautify() && Buffer.length current > 0 &&
-    (!between_com || not(null_comment current_s)) then
+  (if Flags.do_beautify() && Buffer.length current_comment > 0 &&
+    (!between_commands || not(null_comment current_s)) then
     let bp = match !comment_begin with
         Some bp -> bp
       | None ->
@@ -390,9 +391,9 @@ let comment_stop ep =
              ++ int ep);
           ep-1 in
     Pp.comments := ((bp,ep),current_s) :: !Pp.comments);
-  Buffer.clear current;
+  Buffer.clear current_comment;
   comment_begin := None;
-  between_com := false
+  between_commands := false
 
 (* Does not unescape!!! *)
 let rec comm_string loc bp = parser
@@ -548,16 +549,16 @@ let rec next_token loc = parser bp
       | KEYWORD ("." | "...") ->
         if not (blank_or_eof s) then
 	  err (set_loc_pos loc bp (ep+1)) Undefined_token;
-	between_com := true;
+	between_commands := true;
       | _ -> ()
       in
       (t, set_loc_pos loc bp ep)
   | [< ' ('-'|'+'|'*' as c); s >] ->
-      let t,new_between_com =
-        if !between_com then process_sequence loc bp c s, true
+      let t,new_between_commands =
+        if !between_commands then process_sequence loc bp c s, true
         else process_chars loc bp c s,false
       in
-      comment_stop bp; between_com := new_between_com; t
+      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)
@@ -590,9 +591,9 @@ 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), _) ->
             let t = process_chars loc bp (Stream.next s) s in
-            let new_between_com = match t with
-              (KEYWORD ("{"|"}"),_) -> !between_com | _ -> false in
-            comment_stop bp; between_com := new_between_com; t
+            let new_between_commands = match t with
+              (KEYWORD ("{"|"}"),_) -> !between_commands | _ -> false in
+            comment_stop bp; between_commands := new_between_commands; t
         | EmptyStream ->
             comment_stop bp; (EOI, set_loc_pos loc bp (bp+1))
 
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 3b4891d9ac..2c05d6a95f 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -34,10 +34,6 @@ type frozen_t
 val freeze : unit -> frozen_t
 val unfreeze : frozen_t -> unit
 
-type com_state
-val com_state: unit -> com_state
-val restore_com_state: com_state -> unit
-
 val xml_output_comment : (string -> unit) Hook.t
 
 val terminal : string -> Tok.t
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index 18bc8d664f..ecf515111c 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -138,12 +138,21 @@ module type LexerSig = sig
     exception E of t
     val to_string : t -> string
   end
+  type comments_state
+  val default_comments_state : comments_state
+  val comments_state : unit -> comments_state
+  val restore_comments_state : comments_state -> unit
 end
 
 ELSE
 
-module type LexerSig =
-  Camlp4.Sig.Lexer with module Loc = CompatLoc and type Token.t = Tok.t
+module type LexerSig = sig
+  include Camlp4.Sig.Lexer with module Loc = CompatLoc and type Token.t = Tok.t
+  type comments_state
+  val default_comments_state : comments_state
+  val comments_state : unit -> comments_state
+  val restore_comments_state : comments_state -> unit
+end
 
 END
 
@@ -162,10 +171,13 @@ module type GrammarSig = sig
       string option * Gramext.g_assoc option * production_rule list
   type extend_statment =
       Gramext.position option * single_extend_statment list
+  type coq_parsable
+  val parsable : char Stream.t -> coq_parsable
   val action : 'a -> action
   val entry_create : string -> 'a entry
-  val entry_parse : 'a entry -> parsable -> 'a
+  val entry_parse : 'a entry -> coq_parsable -> 'a
   val entry_print : Format.formatter -> 'a entry -> unit
+  val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b
   val srules' : production_rule list -> symbol
   val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
 end
@@ -181,14 +193,33 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct
       string option * Gramext.g_assoc option * production_rule list
   type extend_statment =
       Gramext.position option * single_extend_statment list
+  type coq_parsable = parsable * L.comments_state ref
+  let parsable c =
+    let state = ref L.default_comments_state in (parsable c, state)
   let action = Gramext.action
   let entry_create = Entry.create
-  let entry_parse e p =
-    try Entry.parse e p
+  let entry_parse e (p,state) =
+    L.restore_comments_state !state;
+    try
+      let c = Entry.parse e p in
+      state := L.comments_state ();
+      L.restore_comments_state L.default_comments_state;
+      c
     with Exc_located (loc,e) ->
+      L.restore_comments_state L.default_comments_state;
       let loc' = Loc.get_loc (Exninfo.info e) in
       let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in
       Loc.raise loc e
+  let with_parsable (p,state) f x =
+    L.restore_comments_state !state;
+    try
+      let a = f x in
+      state := L.comments_state ();
+      L.restore_comments_state L.default_comments_state;
+      a
+    with e ->
+      L.restore_comments_state L.default_comments_state;
+      raise e
 
   let entry_print ft x = Entry.print ft x
   let srules' = Gramext.srules
@@ -202,12 +233,13 @@ module type GrammarSig = sig
     with module Loc = CompatLoc and type Token.t = Tok.t
   type 'a entry = 'a Entry.t
   type action = Action.t
-  type parsable
-  val parsable : char Stream.t -> parsable
+  type coq_parsable
+  val parsable : char Stream.t -> coq_parsable
   val action : 'a -> action
   val entry_create : string -> 'a entry
-  val entry_parse : 'a entry -> parsable -> 'a
+  val entry_parse : 'a entry -> coq_parsable -> 'a
   val entry_print : Format.formatter -> 'a entry -> unit
+  val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b
   val srules' : production_rule list -> symbol
 end
 
@@ -217,13 +249,31 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct
   include Camlp4.Struct.Grammar.Static.Make (L)
   type 'a entry = 'a Entry.t
   type action = Action.t
-  type parsable = char Stream.t
-  let parsable s = s
+  type comments_state = int option * string * bool * ((int * int) * string) list
+  type coq_parsable = char Stream.t * L.comments_state ref
+  let parsable s = let state = ref L.default_comments_state in (s, state)
   let action = Action.mk
   let entry_create = Entry.mk
-  let entry_parse e s =
-    try parse e (*FIXME*)CompatLoc.ghost s
-    with Exc_located (loc,e) -> raise_coq_loc loc e
+  let entry_parse e (s,state) =
+    L.restore_comments_state !state;
+    try
+      let c = parse e (*FIXME*)CompatLoc.ghost s in
+      state := L.comments_state ();
+      L.restore_comments_state L.default_comments_state;
+      c
+    with Exc_located (loc,e) ->
+      L.restore_comments_state L.default_comments_state;
+      raise_coq_loc loc e
+  let with_parsable (p,state) f x =
+    L.restore_comments_state !state;
+    try
+      let a = f x in
+      state := L.comments_state ();
+      L.restore_comments_state L.default_comments_state;
+      a
+    with e ->
+      L.restore_comments_state L.default_comments_state;
+      raise e
   let entry_print ft x = Entry.print ft x
   let srules' = srules (entry_create "dummy")
 end
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 69d68bd357..bdcfa8336d 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -23,7 +23,7 @@ type input_buffer = {
   mutable str : string; (* buffer of already read characters *)
   mutable len : int;    (* number of chars in the buffer *)
   mutable bols : int list; (* offsets in str of beginning of lines *)
-  mutable tokens : Gram.parsable; (* stream of tokens *)
+  mutable tokens : Gram.coq_parsable; (* stream of tokens *)
   mutable start : int } (* stream count of the first char of the buffer *)
 
 (* Double the size of the buffer. *)
@@ -274,10 +274,12 @@ let rec discard_to_dot () =
     | End_of_input -> raise End_of_input
     | e when CErrors.noncritical e -> ()
 
-let read_sentence () =
+let read_eval_sentence () =
   try
-    let (loc, _ as r) = Vernac.parse_sentence (top_buffer.tokens, None) in
-    CWarnings.set_current_loc loc; r
+    let input = (top_buffer.tokens, None) in
+    let (loc, _ as r) = Vernac.parse_sentence input in
+    CWarnings.set_current_loc loc;
+    Vernac.eval_expr input r
   with reraise ->
     let reraise = CErrors.push reraise in
     discard_to_dot ();
@@ -298,7 +300,7 @@ let do_vernac () =
   if !print_emacs then top_stderr (str (top_buffer.prompt()));
   resynch_buffer top_buffer;
   try
-    Vernac.eval_expr (read_sentence ())
+    read_eval_sentence ()
   with
     | End_of_input | CErrors.Quit ->
         top_stderr (fnl ()); raise CErrors.Quit
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 00554da308..e40353e0f9 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -18,7 +18,7 @@ type input_buffer = {
   mutable str : string; (** buffer of already read characters *)
   mutable len : int;    (** number of chars in the buffer *)
   mutable bols : int list; (** offsets in str of begining of lines *)
-  mutable tokens : Pcoq.Gram.parsable; (** stream of tokens *)
+  mutable tokens : Pcoq.Gram.coq_parsable; (** stream of tokens *)
   mutable start : int } (** stream count of the first char of the buffer *)
 
 (** The input buffer of stdin. *)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index bdd834d52f..5db6042371 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -124,7 +124,7 @@ let set_formatter_translator() =
   Format.set_formatter_output_functions out (fun () -> flush ch);
   Format.set_max_boxes max_int
 
-let pr_new_syntax loc ocom =
+let pr_new_syntax_in_context loc ocom =
   let loc = Loc.unloc loc in
   if !beautify_file then set_formatter_translator();
   let fs = States.freeze ~marshallable:`No in
@@ -138,20 +138,20 @@ let pr_new_syntax loc ocom =
   States.unfreeze fs;
   Format.set_formatter_out_channel stdout
 
+let pr_new_syntax (po,_) loc ocom =
+  (* Reinstall the context of parsing which includes the bindings of comments to locations *)
+  Pcoq.Gram.with_parsable po (pr_new_syntax_in_context loc) ocom
+
 let save_translator_coqdoc () =
   (* translator state *)
   let ch = !chan_beautify in
-  let cl = !Pp.comments in
-  let cs = CLexer.com_state() in
   (* end translator state *)
   let coqdocstate = CLexer.location_table () in
-  ch,cl,cs,coqdocstate
+  ch,coqdocstate
 
-let restore_translator_coqdoc (ch,cl,cs,coqdocstate) =
+let restore_translator_coqdoc (ch,coqdocstate) =
   if !Flags.beautify_file then close_out !chan_beautify;
   chan_beautify := ch;
-  Pp.comments := cl;
-  CLexer.restore_com_state cs;
   CLexer.restore_location_table coqdocstate
 
 (* For coqtop -time, we display the position in the file,
@@ -182,7 +182,7 @@ let print_cmd_header loc com =
   Pp.pp_with !Pp_control.std_ft (pp_cmd_header loc com);
   Format.pp_print_flush !Pp_control.std_ft ()
 
-let rec vernac_com checknav (loc,com) =
+let rec vernac_com input checknav (loc,com) =
   let interp = function
     | VernacLoad (verbosely, fname) ->
 	let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
@@ -194,7 +194,6 @@ let rec vernac_com checknav (loc,com) =
 	if !Flags.beautify_file then
 	  begin
 	    chan_beautify := open_out (f^beautify_suffix);
-	    Pp.comments := []
           end;
 	begin
 	  try
@@ -214,13 +213,11 @@ let rec vernac_com checknav (loc,com) =
   in
     try
       checknav loc com;
-      if do_beautify () then pr_new_syntax loc (Some com);
+      if do_beautify () then pr_new_syntax input loc (Some com);
       (* XXX: This is not 100% correct if called from an IDE context *)
       if !Flags.time then print_cmd_header loc com;
       let com = if !Flags.time then VernacTime (loc,com) else com in
-      let a = CLexer.com_state () in
-      interp com;
-      CLexer.restore_com_state a
+      interp com
     with reraise ->
       let (reraise, info) = CErrors.push reraise in
       Format.set_formatter_out_channel stdout;
@@ -240,7 +237,7 @@ and read_vernac_file verbosely s =
     while true do
       let loc_ast = parse_sentence input in
       CWarnings.set_current_loc (fst loc_ast);
-      vernac_com checknav loc_ast;
+      vernac_com input checknav loc_ast;
     done
   with any ->   (* whatever the exception *)
     let (e, info) = CErrors.push any in
@@ -249,7 +246,7 @@ and read_vernac_file verbosely s =
     match e with
       | End_of_input ->
           if do_beautify () then
-            pr_new_syntax (Loc.make_loc (max_int,max_int)) None
+            pr_new_syntax input (Loc.make_loc (max_int,max_int)) None
       | reraise ->
 	 iraise (disable_drop e, info)
 
@@ -264,7 +261,7 @@ let checknav loc ast =
   if is_deep_navigation_vernac ast then
     user_error loc "Navigation commands forbidden in nested commands"
 
-let eval_expr loc_ast = vernac_com checknav loc_ast
+let eval_expr input loc_ast = vernac_com input checknav loc_ast
 
 (* XML output hooks *)
 let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore ()
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 7bfddd9470..2fd86ddc22 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -11,7 +11,7 @@
 (** Read a vernac command on the specified input (parse only).
    Raises [End_of_file] if EOF (or Ctrl-D) is reached. *)
 
-val parse_sentence : Pcoq.Gram.parsable * in_channel option ->
+val parse_sentence : Pcoq.Gram.coq_parsable * in_channel option ->
  Loc.t * Vernacexpr.vernac_expr
 
 (** Reads and executes vernac commands from a stream.
@@ -21,7 +21,7 @@ exception End_of_input
 
 val just_parsing : bool ref
 
-val eval_expr : Loc.t * Vernacexpr.vernac_expr -> unit
+val eval_expr : Pcoq.Gram.coq_parsable * in_channel option -> Loc.t * Vernacexpr.vernac_expr -> unit
 
 (** Set XML hooks *)
 val xml_start_library : (unit -> unit) Hook.t
-- 
cgit v1.2.3


From b8ae2de5be242bbd1e34ec974627c81f99b16d23 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 8 Oct 2016 22:51:09 +0200
Subject: Moving Pp.comments to CLexer so that Pp is purer (no more side-effect
 done by the Ppcmd_comment token) and so that lexing/parsing side-effects are
 collected at the same place, i.e. in CLexer.

---
 lib/pp.ml            | 18 +++---------------
 lib/pp.mli           |  3 +--
 parsing/cLexer.ml4   | 17 ++++++++++++++---
 parsing/cLexer.mli   |  4 ++++
 printing/ppconstr.ml |  2 +-
 printing/pputils.ml  |  6 +++++-
 toplevel/vernac.ml   |  5 ++++-
 7 files changed, 32 insertions(+), 23 deletions(-)

diff --git a/lib/pp.ml b/lib/pp.ml
index 7f4bc149dc..8291e7462a 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -77,17 +77,6 @@ open Pp_control
    \end{description}
  *)
 
-let comments = ref []
-
-let rec split_com comacc acc pos = function
-    [] -> comments := List.rev acc; comacc
-  | ((b,e),c as com)::coms ->
-      (* Take all comments that terminates before pos, or begin exactly
-         at pos (used to print comments attached after an expression) *)
-      if e<=pos || pos=b then split_com (c::comacc) acc pos coms
-      else  split_com comacc (com::acc) pos coms
-
-
 type block_type =
   | Pp_hbox of int
   | Pp_vbox of int
@@ -111,7 +100,7 @@ type 'a ppcmd_token =
   | Ppcmd_open_box of block_type
   | Ppcmd_close_box
   | Ppcmd_close_tbox
-  | Ppcmd_comment of int
+  | Ppcmd_comment of string list
   | Ppcmd_open_tag of Tag.t
   | Ppcmd_close_tag
 
@@ -177,7 +166,7 @@ let tab () = Glue.atom(Ppcmd_set_tab)
 let fnl () = Glue.atom(Ppcmd_force_newline)
 let pifb () = Glue.atom(Ppcmd_print_if_broken)
 let ws n = Glue.atom(Ppcmd_white_space n)
-let comment n = Glue.atom(Ppcmd_comment n)
+let comment l = Glue.atom(Ppcmd_comment l)
 
 (* derived commands *)
 let mt () = Glue.empty
@@ -321,8 +310,7 @@ let pp_dirs ?pp_tag ft =
         com_brk ft; Format.pp_force_newline ft ()
     | Ppcmd_print_if_broken   ->
         com_if ft (Lazy.from_fun(fun()->Format.pp_print_if_newline ft ()))
-    | Ppcmd_comment i         ->
-        let coms = split_com [] [] i !comments in
+    | Ppcmd_comment coms      ->
 (*        Format.pp_open_hvbox ft 0;*)
         List.iter (pr_com ft) coms(*;
         Format.pp_close_box ft ()*)
diff --git a/lib/pp.mli b/lib/pp.mli
index 3bd560812e..f607e99dba 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -23,8 +23,7 @@ val ws    : int -> std_ppcmds
 val mt    : unit -> std_ppcmds
 val ismt  : std_ppcmds -> bool
 
-val comment  : int -> std_ppcmds
-val comments : ((int * int) * string) list ref
+val comment  : string list -> std_ppcmds
 
 (** {6 Manipulation commands} *)
 
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 777cdc9bf7..181c4b7fd8 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -340,18 +340,29 @@ let comm_loc bp = match !comment_begin with
 | None -> comment_begin := Some bp
 | _ -> ()
 
+let comments = ref []
 let current_comment = Buffer.create 8192
 let between_commands = ref true
 
+let rec split_comments comacc acc pos = function
+    [] -> comments := List.rev acc; comacc
+  | ((b,e),c as com)::coms ->
+      (* Take all comments that terminates before pos, or begin exactly
+         at pos (used to print comments attached after an expression) *)
+      if e<=pos || pos=b then split_comments (c::comacc) acc pos coms
+      else split_comments comacc (com::acc) pos coms
+
+let extract_comments pos = split_comments [] [] pos !comments
+
 type comments_state = int option * string * bool * ((int * int) * string) list
 let restore_comments_state (o,s,b,c) =
   comment_begin := o;
   Buffer.clear current_comment; Buffer.add_string current_comment s;
   between_commands := b;
-  Pp.comments := c
+  comments := c
 let default_comments_state = (None,"",true,[])
 let comments_state () =
-  let s = (!comment_begin, Buffer.contents current_comment, !between_commands, !Pp.comments) in
+  let s = (!comment_begin, Buffer.contents current_comment, !between_commands, !comments) in
   restore_comments_state default_comments_state; s
 
 let real_push_char c = Buffer.add_char current_comment c
@@ -390,7 +401,7 @@ let comment_stop ep =
              ++ str current_s ++str"' ending at  "
              ++ int ep);
           ep-1 in
-    Pp.comments := ((bp,ep),current_s) :: !Pp.comments);
+    comments := ((bp,ep),current_s) :: !comments);
   Buffer.clear current_comment;
   comment_begin := None;
   between_commands := false
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 2c05d6a95f..3ad49eb74a 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -36,6 +36,10 @@ val unfreeze : frozen_t -> unit
 
 val xml_output_comment : (string -> unit) Hook.t
 
+(* Retrieve the comments lexed at a given location of the stream
+   currently being processeed *)
+val extract_comments : int -> string list
+
 val terminal : string -> Tok.t
 
 (** The lexer of Coq: *)
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index fa5a708995..c94650f1ee 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -129,7 +129,7 @@ end) = struct
     str "`" ++ str hd ++ c ++ str tl
 
   let pr_com_at n =
-    if Flags.do_beautify() && not (Int.equal n 0) then comment n
+    if Flags.do_beautify() && not (Int.equal n 0) then comment (CLexer.extract_comments n)
     else mt()
 
   let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
diff --git a/printing/pputils.ml b/printing/pputils.ml
index 906b463a85..57a1d957e0 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -11,5 +11,9 @@ open Pp
 let pr_located pr (loc, x) =
   if Flags.do_beautify () && loc <> Loc.ghost then
     let (b, e) = Loc.unloc loc in
-    Pp.comment b ++ pr x ++ Pp.comment e
+    (* Side-effect: order matters *)
+    let before = Pp.comment (CLexer.extract_comments b) in
+    let x = pr x in
+    let after = Pp.comment (CLexer.extract_comments e) in
+    before ++ x ++ after
   else pr x
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 5db6042371..b8e44db9a7 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -128,11 +128,14 @@ let pr_new_syntax_in_context loc ocom =
   let loc = Loc.unloc loc in
   if !beautify_file then set_formatter_translator();
   let fs = States.freeze ~marshallable:`No in
+  (* Side-effect: order matters *)
+  let before = comment (CLexer.extract_comments (fst loc)) in
   let com = match ocom with
     | Some com -> Ppvernac.pr_vernac com
     | None -> mt() in
+  let after = comment (CLexer.extract_comments (snd loc)) in
   if !beautify_file then
-    Pp.msg_with !Pp_control.std_ft (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
+    Pp.msg_with !Pp_control.std_ft (hov 0 (before ++ com ++ after))
   else
     Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
   States.unfreeze fs;
-- 
cgit v1.2.3


From eb87cdaeb252d758b6a76b36867254823169576b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 9 Oct 2016 08:18:52 +0200
Subject: A tentative fix for #5102 (bullets parsing broken by calls to
 parse_entry).

More precisely, commands that calls parse_entry put the lexer in an
inconsistent state, breaking the lexing of bullet which relies on it.

(Not to be pushed to v8.6 which has a better fix).
---
 stm/stm.ml         | 6 +++++-
 toplevel/vernac.ml | 4 +++-
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 95cecb7fe2..3bcefa6388 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -109,9 +109,13 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } =
     set_id_for_feedback ?route (Feedback.State id);
     Aux_file.record_in_aux_set_at loc;
     prerr_endline (fun () -> "interpreting " ^ string_of_ppcmds(pr_vernac expr));
-    try Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr))
+    let a = Lexer.com_state () in
+    try
+      Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr));
+      Lexer.restore_com_state a
     with e ->
       let e = Errors.push e in
+      Lexer.restore_com_state a;
       iraise Hooks.(call_process_error_once e)
   end
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 1f7b947e93..177f3c775b 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -230,7 +230,9 @@ let rec vernac_com checknav (loc,com) =
       if do_beautify () then pr_new_syntax loc (Some com);
       if !Flags.time then display_cmd_header loc com;
       let com = if !Flags.time then VernacTime [loc,com] else com in
-      interp com
+      let a = Lexer.com_state () in
+      interp com;
+      Lexer.restore_com_state a
     with reraise ->
       let (reraise, info) = Errors.push reraise in
       Format.set_formatter_out_channel stdout;
-- 
cgit v1.2.3


From c70fe0c63238128a6bb98b9fa75445c4b71c7af5 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Mon, 10 Oct 2016 10:53:51 +0200
Subject: Fix #4416: - Incorrect "Error: Incorrect number of goals"

In `Ftactic` the number of results could desynchronise with the number
of goals when some goals were solved by side effect in a different
branch of a `DISPATCH`.

See [coq-bugs#4416](https://coq.inria.fr/bugs/show_bug.cgi?id=4416).
---
 lib/monad.ml         | 11 +++++++++++
 lib/monad.mli        |  3 +++
 proofs/proofview.ml  |  4 ++++
 proofs/proofview.mli |  4 ++++
 tactics/ftactic.ml   | 23 +++++++++++++++++++----
 5 files changed, 41 insertions(+), 4 deletions(-)

diff --git a/lib/monad.ml b/lib/monad.ml
index a1714a41b3..2e55e9698c 100644
--- a/lib/monad.ml
+++ b/lib/monad.ml
@@ -64,6 +64,9 @@ module type ListS = sig
       its second argument in a tail position. *)
   val iter : ('a -> unit t) -> 'a list -> unit t
 
+  (** Like the regular {!CList.map_filter}. The monadic effects are threaded left*)
+  val map_filter : ('a -> 'b option t) -> 'a list -> 'b list t
+
 
   (** {6 Two-list iterators} *)
 
@@ -138,6 +141,14 @@ module Make (M:Def) : S with type +'a t = 'a M.t = struct
       | a::b::l -> f a >> f b >> iter f l
 
 
+    let rec map_filter f = function
+      | [] -> return []
+      | a::l ->
+        f a >>= function
+        | None -> map_filter f l
+        | Some b ->
+          map_filter f l >>= fun filtered ->
+          return (b::filtered)
 
     let rec fold_left2 r f x l1 l2 =
       match l1,l2 with
diff --git a/lib/monad.mli b/lib/monad.mli
index c8655efa04..f7de71f53a 100644
--- a/lib/monad.mli
+++ b/lib/monad.mli
@@ -66,6 +66,9 @@ module type ListS = sig
       its second argument in a tail position. *)
   val iter : ('a -> unit t) -> 'a list -> unit t
 
+  (** Like the regular {!CList.map_filter}. The monadic effects are threaded left*)
+  val map_filter : ('a -> 'b option t) -> 'a list -> 'b list t
+
 
   (** {6 Two-list iterators} *)
 
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 483f82113d..ae7e2b79a8 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -1016,6 +1016,10 @@ module Goal = struct
     in
     tclUNIT (CList.map_filter map step.comb)
 
+  let unsolved { self=self } =
+    tclEVARMAP >>= fun sigma ->
+    tclUNIT (not (Option.is_empty (advance sigma self)))
+
   (* compatibility *)
   let goal { self=self } = self
 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 2157459f46..1a367f4eac 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -466,6 +466,10 @@ module Goal : sig
   (** Recover the list of current goals under focus, without evar-normalization *)
   val goals : [ `LZ ] t tactic list tactic
 
+  (** [unsolved g] is [true] if [g] is still unsolved in the current
+      proof state. *)
+  val unsolved : 'a t -> bool tactic
+
   (** Compatibility: avoid if possible *)
   val goal : [ `NF ] t -> Evar.t
 
diff --git a/tactics/ftactic.ml b/tactics/ftactic.ml
index 8e42dcba74..418dacb48b 100644
--- a/tactics/ftactic.ml
+++ b/tactics/ftactic.ml
@@ -29,13 +29,28 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function
   | Uniform x ->
     (** We dispatch the uniform result on each goal under focus, as we know
         that the [m] argument was actually dependent. *)
-    Proofview.Goal.goals >>= fun l ->
-    let ans = List.map (fun _ -> x) l in
+    Proofview.Goal.goals >>= fun goals ->
+    let ans = List.map (fun g -> (g,x)) goals in
     Proofview.tclUNIT ans
-  | Depends l -> Proofview.tclUNIT l
+  | Depends l ->
+    Proofview.Goal.goals >>= fun goals ->
+    Proofview.tclUNIT (List.combine goals l)
+  in
+  (* After the tactic has run, some goals which were previously
+     produced may have been solved by side effects. The values
+     attached to such goals must be discarded, otherwise the list of
+     result would not have the same length as the list of focused
+     goals, which is an invariant of the [Ftactic] module. It is the
+     reason why a goal is attached to each result above. *)
+  let filter (g,x) =
+    g >>= fun g ->
+    Proofview.Goal.unsolved g >>= function
+    | true -> Proofview.tclUNIT (Some x)
+    | false -> Proofview.tclUNIT None
   in
   Proofview.tclDISPATCHL (List.map f l) >>= fun l ->
-  Proofview.tclUNIT (Depends (List.concat l))
+  Proofview.Monad.List.map_filter filter (List.concat l) >>= fun filtered ->
+  Proofview.tclUNIT (Depends filtered)
 
 let nf_enter f =
   bind (Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l))
-- 
cgit v1.2.3


From 009718d9d0130a967261ae5d2484985522fc2f7c Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 10 Oct 2016 10:58:09 +0200
Subject: Add test file for #4416.

---
 test-suite/bugs/closed/4416.v | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 test-suite/bugs/closed/4416.v

diff --git a/test-suite/bugs/closed/4416.v b/test-suite/bugs/closed/4416.v
new file mode 100644
index 0000000000..b97a8ce640
--- /dev/null
+++ b/test-suite/bugs/closed/4416.v
@@ -0,0 +1,3 @@
+Goal exists x, x.
+unshelve refine (ex_intro _ _ _); match goal with _ => refine (_ _) end.
+(* Error: Incorrect number of goals (expected 2 tactics). *)
\ No newline at end of file
-- 
cgit v1.2.3


From e3798c52c3bd52d43fa84feedd7caaa4def57db8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 10 Oct 2016 15:47:43 +0200
Subject: Fixing #5133 (error reporting delayed).

I wrongly moved call to the function interpreting commands within a
different try-with block in 8a8caba36e.
---
 toplevel/coqloop.ml | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index bdcfa8336d..71e1f9593d 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -274,12 +274,10 @@ let rec discard_to_dot () =
     | End_of_input -> raise End_of_input
     | e when CErrors.noncritical e -> ()
 
-let read_eval_sentence () =
+let read_sentence input =
   try
-    let input = (top_buffer.tokens, None) in
     let (loc, _ as r) = Vernac.parse_sentence input in
-    CWarnings.set_current_loc loc;
-    Vernac.eval_expr input r
+    CWarnings.set_current_loc loc; r
   with reraise ->
     let reraise = CErrors.push reraise in
     discard_to_dot ();
@@ -300,7 +298,8 @@ let do_vernac () =
   if !print_emacs then top_stderr (str (top_buffer.prompt()));
   resynch_buffer top_buffer;
   try
-    read_eval_sentence ()
+    let input = (top_buffer.tokens, None) in
+    Vernac.eval_expr input (read_sentence input)
   with
     | End_of_input | CErrors.Quit ->
         top_stderr (fnl ()); raise CErrors.Quit
-- 
cgit v1.2.3


From b247761476c4b36f0945c19c23c171ea57701178 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 6 Oct 2016 18:02:25 +0200
Subject: Fix for bug #4863, update the Proofview's env with

side_effects. Partial solution to the handling of side effects
in proofview.
---
 kernel/entries.mli            |  7 ++++++-
 kernel/safe_typing.ml         |  7 -------
 proofs/proofview.ml           | 28 ++++++++++++++++++++++++++--
 test-suite/bugs/closed/4863.v | 32 ++++++++++++++++++++++++++++++++
 4 files changed, 64 insertions(+), 10 deletions(-)
 create mode 100644 test-suite/bugs/closed/4863.v

diff --git a/kernel/entries.mli b/kernel/entries.mli
index f94068f31e..8e8e97d615 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -97,7 +97,12 @@ type module_entry =
   | MExpr of
       module_params_entry * module_struct_entry * module_struct_entry option
 
-type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ]
+
+type seff_env =
+  [ `Nothing
+  (* The proof term and its universes.
+     Same as the constant_body's but not in an ephemeron *)
+  | `Opaque of Constr.t * Univ.universe_context_set ]
 
 type side_eff =
   | SEsubproof of constant * Declarations.constant_body * seff_env
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 927278965f..8b28cd87bd 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -222,13 +222,6 @@ let inline_private_constants_in_constr = Term_typing.inline_side_effects
 let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects
 let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x)
 
-let constant_entry_of_private_constant = function
-  | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } ->
-      [ kn, Term_typing.constant_entry_of_side_effect cb eff_env ]
-  | { Entries.eff = Entries.SEscheme (l,_) } ->
-      List.map (fun (_,kn,cb,eff_env) ->
-        kn, Term_typing.constant_entry_of_side_effect cb eff_env) l
-
 let private_con_of_con env c =
   let cbo = Environ.lookup_constant c env.env in
   { Entries.from_env = CEphemeron.create env.revstruct;
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index ae7e2b79a8..91905be627 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -1071,6 +1071,23 @@ struct
   let (pr_constrv,pr_constr) =
     Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") ()
 
+  (* Get the side-effect's constant declarations to update the monad's
+   * environmnent *)
+  let add_if_undefined kn cb env =
+    try ignore(Environ.lookup_constant kn env); env
+    with Not_found -> Environ.add_constant kn cb env
+
+  (* Add the side effects to the monad's environment, if not already done. *)
+  let add_side_effect env = function
+    | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } ->
+      add_if_undefined kn cb env
+    | { Entries.eff = Entries.SEscheme (l,_) } ->
+      List.fold_left (fun env (_,kn,cb,eff_env) ->
+          add_if_undefined kn cb env) env l
+
+  let add_side_effects env effects =
+    List.fold_left (fun env eff -> add_side_effect env eff) env effects
+
   let refine ?(unsafe = true) f = Goal.enter begin fun gl ->
     let sigma = Goal.sigma gl in
     let env = Goal.env gl in
@@ -1083,6 +1100,10 @@ struct
     let (sigma, c) = f (Evd.reset_future_goals sigma) in
     let evs = Evd.future_goals sigma in
     let evkmain = Evd.principal_future_goal sigma in
+    (** Redo the effects in sigma in the monad's env *)
+    let privates_csts = Evd.eval_side_effects sigma in
+    let sideff = Safe_typing.side_effects_of_private_constants privates_csts in
+    let env = add_side_effects env sideff in
     (** Check that the introduced evars are well-typed *)
     let fold accu ev = typecheck_evar ev env accu in
     let sigma = if unsafe then sigma else CList.fold_left fold sigma evs in
@@ -1109,8 +1130,11 @@ struct
     let comb = undefined sigma (CList.rev evs) in
     let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in
     let open Proof in
-    InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)))) >>
-    Pv.modify (fun ps -> { ps with solution = sigma; comb; })
+    InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"simple refine"++spc()++
+                                                 Hook.get pr_constrv env sigma c)))) >>
+      (** We reset the logical environment extended with the effects. *)
+      Env.set (Environ.reset_context env) >>
+      Pv.modify (fun ps -> { ps with solution = sigma; comb; })
   end
 
   (** Useful definitions *)
diff --git a/test-suite/bugs/closed/4863.v b/test-suite/bugs/closed/4863.v
new file mode 100644
index 0000000000..e884355fde
--- /dev/null
+++ b/test-suite/bugs/closed/4863.v
@@ -0,0 +1,32 @@
+Require Import Classes.DecidableClass.
+
+Inductive Foo : Set :=
+| foo1 | foo2.
+
+Instance Decidable_sumbool : forall P, {P}+{~P} -> Decidable P.
+Proof.
+  intros P H.
+  refine (Build_Decidable _ (if H then true else false) _).
+  intuition congruence.
+Qed.
+
+Hint Extern 100 ({?A = ?B}+{~ ?A = ?B}) => abstract (abstract (abstract (decide equality))) : typeclass_instances.
+
+Goal forall (a b : Foo), {a=b}+{a<>b}.
+intros.
+abstract (abstract (decide equality)). (*abstract works here*)
+Qed.
+
+Check ltac:(abstract (exact I)) : True.
+
+Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b).
+intros.
+split. typeclasses eauto. typeclasses eauto. Qed.
+
+Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b).
+intros.
+split.
+refine _.
+refine _.
+Defined.
+(*fails*)
-- 
cgit v1.2.3


From af3538f0c6decdccd47abcdeb7b7eeaff64b69b5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 11 Oct 2016 12:40:31 +0200
Subject: Reverting generalization and cleaning of the return clause inference
 in v8.6.

The move to systematically trying small inversion first bumps
sometimes as feared to the weakness of unification (see #5107).

----

Revert "Posssible abstractions over goal variables when inferring match return clause."
This reverts commit 0658ba7b908dad946200f872f44260d0e4893a94.

Revert "Trying an abstracting dependencies heuristic for the match return clause even when no type constraint is given."
This reverts commit 292f365185b7acdee79f3ff7b158551c2764c548.

Revert "Trying a no-inversion no-dependency heuristic for match return clause."
This reverts commit 2422aeb2b59229891508f35890653a9737988c00.
---
 pretyping/cases.ml          | 87 +++++++++++++++++++--------------------------
 test-suite/success/Case13.v | 38 --------------------
 2 files changed, 36 insertions(+), 89 deletions(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 7e33cc1d4a..98d3000885 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1870,22 +1870,16 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon =
 
 (* We put the tycon inside the arity signature, possibly discovering dependencies. *)
 
-let add_subst c len (rel_subst,var_subst) =
-  match kind_of_term c with
-  | Rel n -> (n,len) :: rel_subst, var_subst
-  | Var id -> rel_subst, (id,len) :: var_subst
-  | _ -> assert false
-
 let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
   let nar = List.fold_left (fun n sign -> Context.Rel.nhyps sign + n) 0 arsign in
-  let (rel_subst,var_subst), len =
+  let subst, len =
     List.fold_right2 (fun (tm, tmtype) sign (subst, len) ->
       let signlen = List.length sign in
 	match kind_of_term tm with
-	  | Rel _ | Var _ when dependent tm c
+	  | Rel n when dependent tm c
 		&& Int.equal signlen 1 (* The term to match is not of a dependent type itself *) ->
-	      (add_subst tm len subst, len - signlen)
-	  | Rel _ | Var _ when signlen > 1 (* The term is of a dependent type,
+	      ((n, len) :: subst, len - signlen)
+	  | Rel n when signlen > 1 (* The term is of a dependent type,
 				      maybe some variable in its type appears in the tycon. *) ->
 	      (match tmtype with
 		  NotInd _ -> (subst, len - signlen)
@@ -1894,36 +1888,28 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
 		      List.fold_left
 			(fun (subst, len) arg ->
 			  match kind_of_term arg with
-			  | Rel _ | Var _ when dependent arg c ->
-			      (add_subst arg len subst, pred len)
+			  | Rel n when dependent arg c ->
+			      ((n, len) :: subst, pred len)
 			  | _ -> (subst, pred len))
 			(subst, len) realargs
 		    in
 		    let subst =
-		      if dependent tm c && List.for_all (fun c -> isRel c || isVar c) realargs
-		      then add_subst tm len subst else subst
+		      if dependent tm c && List.for_all isRel realargs
+		      then (n, len) :: subst else subst
 		    in (subst, pred len))
 	  | _ -> (subst, len - signlen))
-      (List.rev tomatchs) arsign (([],[]), nar)
+      (List.rev tomatchs) arsign ([], nar)
   in
   let rec predicate lift c =
     match kind_of_term c with
       | Rel n when n > lift ->
 	  (try
 	      (* Make the predicate dependent on the matched variable *)
-	      let idx = Int.List.assoc (n - lift) rel_subst in
+	      let idx = Int.List.assoc (n - lift) subst in
 		mkRel (idx + lift)
 	    with Not_found ->
-	      (* A variable that is not matched, lift over the arsign *)
+	      (* A variable that is not matched, lift over the arsign. *)
 	      mkRel (n + nar))
-      | Var id ->
-	  (try
-	      (* Make the predicate dependent on the matched variable *)
-	      let idx = Id.List.assoc id var_subst in
-		mkRel (idx + lift)
-	    with Not_found ->
-	      (* A variable that is not matched *)
-	      c)
       | _ ->
 	  map_constr_with_binders succ predicate lift c
   in
@@ -1944,39 +1930,38 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
 
 let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
   let preds =
-    match pred with
+    match pred, tycon with
     (* No return clause *)
-    | None ->
-        let sigma,t =
-          match tycon with
-          | Some t -> sigma, t
-          | None ->
-             (* No type constraint: we first create a generic evar type constraint *)
-             let src = (loc, Evar_kinds.CasesType false) in
-             let sigma = Sigma.Unsafe.of_evar_map sigma in
-             let Sigma ((t, _), sigma, _) = new_type_evar env sigma univ_flexible_alg ~src in
-             let sigma = Sigma.to_evar_map sigma in
-             sigma, t in
-        (* First strategy: we build an "inversion" predicate, also replacing the *)
-        (* dependencies with existential variables *)
+    | None, Some t when not (noccur_with_meta 0 max_int t) ->
+	(* If the tycon is not closed w.r.t real variables, we try *)
+        (* two different strategies *)
+	(* First strategy: we build an "inversion" predicate *)
 	let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
 	(* Optional second strategy: we abstract the tycon wrt to the dependencies *)
         let p2 =
           prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
-        (* Third strategy: we take the type constraint as it is; of course we could *)
-        (* need something inbetween, abstracting some but not all of the dependencies *)
-        (* the "inversion" strategy deals with that but unification may not be *)
-        (* powerful enough so strategy 2 and 3 helps; moreover, inverting does not *)
-        (* work (yet) when a constructor has a type not precise enough for the inversion *)
-        (* see log message for details *)
-        let pred3 = lift (List.length (List.flatten arsign)) t in
 	(match p2 with
-	 | Some (sigma2,pred2) when not (Constr.equal pred2 pred3) ->
-             [sigma1, pred1; sigma2, pred2; sigma, pred3]
-	 | _ ->
-             [sigma1, pred1; sigma, pred3])
+	 | Some (sigma2,pred2) -> [sigma1, pred1; sigma2, pred2]
+	 | None -> [sigma1, pred1])
+    | None, _ ->
+	(* No dependent type constraint, or no constraints at all: *)
+	(* we use two strategies *)
+        let sigma,t = match tycon with
+	| Some t -> sigma,t
+	| None -> 
+          let sigma = Sigma.Unsafe.of_evar_map sigma in
+          let Sigma ((t, _), sigma, _) =
+	    new_type_evar env sigma univ_flexible_alg ~src:(loc, Evar_kinds.CasesType false) in
+          let sigma = Sigma.to_evar_map sigma in
+	    sigma, t
+	in
+        (* First strategy: we build an "inversion" predicate *)
+	let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
+	(* Second strategy: we use the evar or tycon as a non dependent pred *)
+        let pred2 = lift (List.length (List.flatten arsign)) t in
+	[sigma1, pred1; sigma, pred2]
     (* Some type annotation *)
-    | Some rtntyp ->
+    | Some rtntyp, _ ->
       (* We extract the signature of the arity *)
       let envar = List.fold_right push_rel_context arsign env in
       let sigma, newt = new_sort_variable univ_flexible_alg sigma in
diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index 356a67efec..8f95484cfd 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -87,41 +87,3 @@ Check fun (x : E) => match x with c => e c end.
 Inductive C' : bool -> Set := c' : C' true.
 Inductive E' (b : bool) : Set := e' :> C' b -> E' b.
 Check fun (x : E' true) => match x with c' => e' true c' end.
-
-(* Check use of the no-dependency strategy when a type constraint is
-   given (and when the "inversion-and-dependencies-as-evars" strategy
-   is not strong enough because of a constructor with a type whose
-   pattern structure is not refined enough for it to be captured by
-   the inversion predicate) *)
-
-Inductive K : bool -> bool -> Type := F : K true true | G x : K x x.
-
-Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y, P y -> Q y z) =>
-        match y with
-        | F  => f y H1
-        | G _ => f y H2
-        end : Q y z.
-
-(* Check use of the maximal-dependency-in-variable strategy even when
-   no explicit type constraint is given (and when the
-   "inversion-and-dependencies-as-evars" strategy is not strong enough
-   because of a constructor with a type whose pattern structure is not
-   refined enough for it to be captured by the inversion predicate) *)
-
-Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z) =>
-        match y with
-        | F  => f y true H1
-        | G b => f y b H2
-        end.
-
-(* Check use of the maximal-dependency-in-variable strategy for "Var"
-   variables *)
-
-Goal forall z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z), Q y z.
-intros z P Q y H1 H2 f.
-Show.
-refine (match y with
-        | F  => f y true H1
-        | G b => f y b H2
-        end).
-Qed.
-- 
cgit v1.2.3


From d226adf01f20ea946bbeac4d4c5cde75a4d77f32 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 11 Oct 2016 11:57:46 +0200
Subject: Fix bug #5123: mark all shelved evars unresolvable

Previously, some splipped through and were caught by unrelated calls to
typeclass resolution.
---
 proofs/proof.ml               |  9 ++++++++-
 proofs/proofview.ml           | 36 ++++++++++++++++++++++--------------
 proofs/proofview.mli          |  8 ++++++--
 test-suite/bugs/closed/5123.v | 31 +++++++++++++++++++++++++++++++
 4 files changed, 67 insertions(+), 17 deletions(-)
 create mode 100644 test-suite/bugs/closed/5123.v

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 0489305aa7..1f094b3391 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -343,13 +343,20 @@ let run_tactic env tac pr =
      they to be marked as unresolvable. *)
   let undef l = List.filter (fun g -> Evd.is_undefined sigma g) l in
   let retrieved = undef (List.rev (Evd.future_goals sigma)) in
-  let shelf = (undef pr.shelf)@retrieved@(undef to_shelve) in
+  let to_shelve = undef to_shelve in
+  let shelf = (undef pr.shelf)@retrieved@to_shelve in
   let proofview =
     List.fold_left
       Proofview.Unsafe.mark_as_goal
       tacticced_proofview
       retrieved
   in
+  let proofview =
+    List.fold_left
+      Proofview.Unsafe.mark_as_unresolvable
+      proofview
+      to_shelve
+  in
   let given_up = pr.given_up@give_up in
   let proofview = Proofview.Unsafe.reset_future_goals proofview in
   { pr with proofview ; shelf ; given_up },(status,info_trace)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index ae7e2b79a8..d166f46b23 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -642,6 +642,18 @@ let unshelve l p =
   let l = undefined p.solution l in
   { p with comb = p.comb@l }
 
+let mark_in_evm ~goal evd content =
+  let info = Evd.find evd content in
+  let info =
+    if goal then
+      { info with Evd.evar_source = match info.Evd.evar_source with
+            | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
+            | loc,_ -> loc,Evar_kinds.GoalEvar }
+    else info
+  in
+  let info = Typeclasses.mark_unresolvable info in
+  Evd.add evd content info
+
 let with_shelf tac =
   let open Proof in
   Pv.get >>= fun pv ->
@@ -654,8 +666,11 @@ let with_shelf tac =
   let fgoals = Evd.future_goals solution in
   let pgoal = Evd.principal_future_goal solution in
   let sigma = Evd.restore_future_goals sigma fgoals pgoal in
-  Pv.set { npv with shelf; solution = sigma } >>
-  tclUNIT (CList.rev_append gls' gls, ans)
+  (* Ensure we mark and return only unsolved goals *)
+  let gls' = undefined sigma (CList.rev_append gls' gls) in
+  let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in
+  let npv = { npv with shelf; solution = sigma } in
+  Pv.set npv >> tclUNIT (gls', ans)
 
 (** [goodmod p m] computes the representative of [p] modulo [m] in the
     interval [[0,m-1]].*)
@@ -893,18 +908,11 @@ module Unsafe = struct
   let reset_future_goals p =
     { p with solution = Evd.reset_future_goals p.solution }
 
-  let mark_as_goal_evm evd content =
-    let info = Evd.find evd content in
-    let info =
-      { info with Evd.evar_source = match info.Evd.evar_source with
-      | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
-      | loc,_ -> loc,Evar_kinds.GoalEvar }
-    in
-    let info = Typeclasses.mark_unresolvable info in
-    Evd.add evd content info
-
   let mark_as_goal p gl =
-    { p with solution = mark_as_goal_evm p.solution gl }
+    { p with solution = mark_in_evm ~goal:true p.solution gl }
+
+  let mark_as_unresolvable p gl =
+    { p with solution = mark_in_evm ~goal:false p.solution gl }
 
 end
 
@@ -1107,7 +1115,7 @@ struct
     let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in
     (** Select the goals *)
     let comb = undefined sigma (CList.rev evs) in
-    let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in
+    let sigma = CList.fold_left (mark_in_evm ~goal:true) sigma comb in
     let open Proof in
     InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)))) >>
     Pv.modify (fun ps -> { ps with solution = sigma; comb; })
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 1a367f4eac..c8d96fe794 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -303,8 +303,9 @@ val guard_no_unifiable : unit tactic
     goals of p *)
 val unshelve : Goal.goal list -> proofview -> proofview
 
-(** [with_shelf tac] executes [tac] and returns its result together with the set
-    of goals shelved by [tac]. The current shelf is unchanged. *)
+(** [with_shelf tac] executes [tac] and returns its result together with
+    the set of goals shelved by [tac]. The current shelf is unchanged
+    and the returned list contains only unsolved goals. *)
 val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic
 
 (** If [n] is positive, [cycle n] puts the [n] first goal last. If [n]
@@ -407,6 +408,9 @@ module Unsafe : sig
   (** Give an evar the status of a goal (changes its source location
       and makes it unresolvable for type classes. *)
   val mark_as_goal : proofview -> Evar.t -> proofview
+
+  (** Make an evar unresolvable for type classes. *)
+  val mark_as_unresolvable : proofview -> Evar.t -> proofview
 end
 
 (** {7 Notations} *)
diff --git a/test-suite/bugs/closed/5123.v b/test-suite/bugs/closed/5123.v
new file mode 100644
index 0000000000..c171a10d10
--- /dev/null
+++ b/test-suite/bugs/closed/5123.v
@@ -0,0 +1,31 @@
+(* IN 8.5pl2 and 8.6 (4da2131), the following shows different typeclass resolution behaviors following an unshelve tactical vs. an Unshelve command: *)
+
+(*Pose an open constr to prevent immediate typeclass resolution in holes:*)
+Tactic Notation "opose" open_constr(x) "as" ident(H) := pose x as H.
+
+Inductive vect A : nat -> Type :=
+| vnil : vect A 0
+| vcons : forall (h:A) (n:nat), vect A n -> vect A (S n).
+
+Class Eqdec A := eqdec : forall a b : A, {a=b}+{a<>b}.
+
+Require Bool.
+
+Instance Bool_eqdec : Eqdec bool := Bool.bool_dec.
+
+Context `{vect_sigT_eqdec : forall A : Type, Eqdec A -> Eqdec {a : nat & vect A a}}.
+
+Typeclasses eauto := debug.
+
+Goal True.
+  unshelve opose (@vect_sigT_eqdec _ _ _ _) as H.
+  all:cycle 2.
+  eapply existT. (*BUG: Why does this do typeclass resolution in the evar?*)
+Abort.
+
+Goal True.
+  opose (@vect_sigT_eqdec _ _ _ _) as H.
+  Unshelve.
+  all:cycle 3.
+  eapply existT. (*This does no typeclass resultion, which is correct.*)
+Abort.
\ No newline at end of file
-- 
cgit v1.2.3


From 2bcae5b7a22019718973f65cafd271f735d3d85b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 11 Oct 2016 16:33:26 +0200
Subject: Fix test-suite file 5123 to fail in case of regression

---
 test-suite/bugs/closed/5123.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/test-suite/bugs/closed/5123.v b/test-suite/bugs/closed/5123.v
index c171a10d10..bcde510ee6 100644
--- a/test-suite/bugs/closed/5123.v
+++ b/test-suite/bugs/closed/5123.v
@@ -21,6 +21,7 @@ Goal True.
   unshelve opose (@vect_sigT_eqdec _ _ _ _) as H.
   all:cycle 2.
   eapply existT. (*BUG: Why does this do typeclass resolution in the evar?*)
+  Focus 5.
 Abort.
 
 Goal True.
@@ -28,4 +29,5 @@ Goal True.
   Unshelve.
   all:cycle 3.
   eapply existT. (*This does no typeclass resultion, which is correct.*)
+  Focus 5.
 Abort.
\ No newline at end of file
-- 
cgit v1.2.3


From 96ed527472c38e92727d8fb6bfc41770c43b762b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 11 Oct 2016 22:11:16 +0200
Subject: Fixing a few confusions on the name of the beautify flag. (It should
 apply also interactively.)

---
 interp/constrextern.ml | 2 +-
 printing/ppvernac.ml   | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e71daef999..afc1c4caf8 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -481,7 +481,7 @@ let explicitize loc inctx impl (cf,f) args =
           (!print_implicits && !print_implicits_explicit_args) ||
           (is_needed_for_correct_partial_application tail imp) ||
 	  (!print_implicits_defensive &&
-	   (not (is_inferable_implicit inctx n imp) || !Flags.beautify_file) &&
+	   (not (is_inferable_implicit inctx n imp) || !Flags.beautify) &&
 	   is_significant_implicit (Lazy.force a))
 	in
         if visible then
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index f4a112a4cb..cfb4e79f03 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -263,7 +263,7 @@ module Make
 
   let pr_decl_notation prc ((loc,ntn),c,scopt) =
     fnl () ++ keyword "where " ++ qs ntn ++ str " := "
-    ++ Flags.without_option Flags.beautify_file prc c ++
+    ++ Flags.without_option Flags.beautify prc c ++
       pr_opt (fun sc -> str ": " ++ str sc) scopt
 
   let pr_binders_arg =
@@ -383,7 +383,7 @@ module Make
     | Some pl -> str"@{" ++ prlist_with_sep spc pr_lident pl ++ str"}"
 
   let pr_rec_definition ((((loc,id),pl),ro,bl,type_,def),ntn) =
-    let pr_pure_lconstr c = Flags.without_option Flags.beautify_file pr_lconstr c in
+    let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in
     let annot = pr_guard_annot pr_lconstr_expr bl ro in
     pr_id id ++ pr_univs pl ++ pr_binders_arg bl ++ annot
     ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
@@ -678,7 +678,7 @@ module Make
       | VernacNotation (_,c,((_,s),l),opt) ->
         return (
           hov 2 (keyword "Notation" ++ spc() ++ qs s ++
-                   str " :=" ++ Flags.without_option Flags.beautify_file pr_constrarg c ++ pr_syntax_modifiers l ++
+                   str " :=" ++ Flags.without_option Flags.beautify pr_constrarg c ++ pr_syntax_modifiers l ++
                    (match opt with
                      | None -> mt()
                      | Some sc -> str" :" ++ spc() ++ str sc))
@@ -760,7 +760,7 @@ module Make
         let pr_constructor (coe,(id,c)) =
           hov 2 (pr_lident id ++ str" " ++
                    (if coe then str":>" else str":") ++
-                   Flags.without_option Flags.beautify_file pr_spc_lconstr c)
+                   Flags.without_option Flags.beautify pr_spc_lconstr c)
         in
         let pr_constructor_list b l = match l with
           | Constructors [] -> mt()
-- 
cgit v1.2.3


From 5539201bf25dec1b5c24634dca581e199caca4e7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 10 Oct 2016 12:02:21 +0200
Subject: Shorter message for "Test Asymmetric Patterns".

But maybe it is that how the "Test" message is elaborated is not
intuitive...
---
 interp/topconstr.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 2b860173a6..79eeacf354 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -22,8 +22,7 @@ open Constrexpr_ops
 let asymmetric_patterns = ref (false)
 let _ = Goptions.declare_bool_option {
   Goptions.optsync = true; Goptions.optdepr = false;
-  Goptions.optname =
-    "Constructors in patterns require all their arguments but no parameters instead of explicit parameters and arguments";
+  Goptions.optname = "no parameters in constructors";
   Goptions.optkey = ["Asymmetric";"Patterns"];
   Goptions.optread = (fun () -> !asymmetric_patterns);
   Goptions.optwrite = (fun a -> asymmetric_patterns:=a);
-- 
cgit v1.2.3


From 55699e2b9a91356b7d43c4096f65fb199777b9a1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 8 Oct 2016 02:21:26 +0200
Subject: Fix bug #4958: [debug auto] should specify hint databases.

---
 tactics/auto.ml   | 11 +++++++++--
 tactics/auto.mli  |  2 --
 tactics/hints.ml  | 53 ++++++++++++++++++++++++++++++++++++++++++++---------
 tactics/hints.mli |  7 ++++---
 4 files changed, 57 insertions(+), 16 deletions(-)

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 962af4b5c5..6d1a1ae28f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -375,7 +375,7 @@ and my_find_search_delta db_list local_db hdc concl =
 	  in List.map (fun x -> (Some flags,x)) l)
       	(local_db::db_list)
 
-and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly})) =
+and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) =
   let tactic = function
     | Res_pf (c,cl) -> unify_resolve_gen poly flags (c,cl)
     | ERes_pf _ -> Proofview.V82.tactic (fun gl -> error "eres_pf")
@@ -394,7 +394,14 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly}))
     | Extern tacast -> 
       conclPattern concl p tacast
   in
-  tclLOG dbg (fun () -> pr_hint t) (run_hint t tactic)
+  let pr_hint () =
+    let origin = match dbname with
+    | None -> mt ()
+    | Some n -> str " (in " ++ str n ++ str ")"
+    in
+    pr_hint t ++ origin
+  in
+  tclLOG dbg pr_hint (run_hint t tactic)
 
 and trivial_resolve dbg mod_delta db_list local_db cl =
   try
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 1608a0ea63..5384140c2a 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -15,8 +15,6 @@ open Pattern
 open Decl_kinds
 open Hints
 
-val priority : ('a * full_hint) list -> ('a * full_hint) list
-
 val default_search_depth : int ref
 
 val auto_flags_of_state : transparent_state -> Unification.unify_flags
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 8f3eb5eb51..d1343f296e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -108,6 +108,7 @@ type 'a with_metadata = {
   poly  : polymorphic;    (** Is the hint polymorpic and hence should be refreshed at each application *)
   pat  : constr_pattern option; (* A pattern for the concl of the Goal *)
   name  : hints_path_atom; (* A potential name to refer to the hint *) 
+  db : string option; (** The database from which the hint comes *)
   code : 'a;     (* the tactic to apply when the concl matches pat *)
 }
 
@@ -410,7 +411,35 @@ let rec subst_hints_path subst hp =
       if p' == p && q' == q then hp else PathOr (p', q')
   | _ -> hp
 
-module Hint_db = struct
+type hint_db_name = string
+
+module Hint_db :
+sig
+type t
+val empty : ?name:hint_db_name -> transparent_state -> bool -> t
+val find : global_reference -> t -> search_entry
+val map_none : t -> full_hint list
+val map_all : global_reference -> t -> full_hint list
+val map_existential : (global_reference * constr array) -> constr -> t -> full_hint list
+val map_eauto : (global_reference * constr array) -> constr -> t -> full_hint list
+val map_auto : (global_reference * constr array) -> constr -> t -> full_hint list
+val add_one : env -> evar_map -> hint_entry -> t -> t
+val add_list : env -> evar_map -> hint_entry list -> t -> t
+val remove_one : global_reference -> t -> t
+val remove_list : global_reference list -> t -> t
+val iter : (global_reference option -> hint_mode array list -> full_hint list -> unit) -> t -> unit
+val use_dn : t -> bool
+val transparent_state : t -> transparent_state
+val set_transparent_state : t -> transparent_state -> t
+val add_cut : hints_path -> t -> t
+val add_mode : global_reference -> hint_mode array -> t -> t
+val cut : t -> hints_path
+val unfolds : t -> Id.Set.t * Cset.t
+val fold : (global_reference option -> hint_mode array list -> full_hint list -> 'a -> 'a) ->
+  t -> 'a -> 'a
+
+end =
+struct
 
   type t = {
     hintdb_state : Names.transparent_state;
@@ -421,20 +450,22 @@ module Hint_db = struct
     hintdb_map : search_entry Constr_map.t;
     (* A list of unindexed entries starting with an unfoldable constant
        or with no associated pattern. *)
-    hintdb_nopat : (global_reference option * stored_data) list
+    hintdb_nopat : (global_reference option * stored_data) list;
+    hintdb_name : string option;
   }
 
   let next_hint_id db =
     let h = db.hintdb_max_id in
     { db with hintdb_max_id = succ db.hintdb_max_id }, h
 
-  let empty st use_dn = { hintdb_state = st;
+  let empty ?name st use_dn = { hintdb_state = st;
 			  hintdb_cut = PathEmpty;
 			  hintdb_unfolds = (Id.Set.empty, Cset.empty);
 			  hintdb_max_id = 0;
 			  use_dn = use_dn;
 			  hintdb_map = Constr_map.empty;
-			  hintdb_nopat = [] }
+			  hintdb_nopat = [];
+			  hintdb_name = name; }
 
   let find key db =
     try Constr_map.find key db.hintdb_map
@@ -502,7 +533,7 @@ module Hint_db = struct
     | _ -> false
 
   let addkv gr id v db =
-    let idv = id, v in
+    let idv = id, { v with db = db.hintdb_name } in
     let k = match gr with
       | Some gr -> if db.use_dn && is_transparent_gr db.hintdb_state gr &&
 	  is_unfold v.code.obj then None else Some gr
@@ -606,8 +637,6 @@ type hint_db = Hint_db.t
 
 type hint_db_table = hint_db Hintdbmap.t ref
 
-type hint_db_name = string
-
 (** Initially created hint databases, for typeclasses and rewrite *)
 
 let typeclasses_db = "typeclass_instances"
@@ -684,6 +713,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
 	    poly = poly;
 	    pat = Some pat;
 	    name = name;
+            db = None;
 	    code = with_uid (Give_exact (c, cty, ctx)); })
 
 let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, cty, ctx) =
@@ -704,6 +734,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
 	    poly = poly;
             pat = Some pat;
 	    name = name;
+            db = None;
             code = with_uid (Res_pf(c,cty,ctx)); })
 	else begin
 	  if not eapply then failwith "make_apply_entry";
@@ -715,6 +746,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
 	     poly = poly;
              pat = Some pat;
 	     name = name;
+             db = None;
              code = with_uid (ERes_pf(c,cty,ctx)); })
         end
     | _ -> failwith "make_apply_entry"
@@ -799,6 +831,7 @@ let make_unfold eref =
      poly = false;
      pat = None;
      name = PathHints [g];
+     db = None;
      code = with_uid (Unfold_nth eref) })
 
 let make_extern pri pat tacast =
@@ -809,6 +842,7 @@ let make_extern pri pat tacast =
      poly = false;
      pat = pat;
      name = PathAny;
+     db = None;
      code = with_uid (Extern tacast) })  
 
 let make_mode ref m = 
@@ -832,6 +866,7 @@ let make_trivial env sigma poly ?(name=PathAny) r =
 	      poly = poly;
               pat = Some (Patternops.pattern_of_constr env ce.evd (clenv_type ce));
 	      name = name;
+              db = None;
               code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) })
 
 
@@ -845,7 +880,7 @@ let make_trivial env sigma poly ?(name=PathAny) r =
 
 let get_db dbname =
   try searchtable_map dbname
-  with Not_found -> Hint_db.empty empty_transparent_state false
+  with Not_found -> Hint_db.empty ~name:dbname empty_transparent_state false
 
 let add_hint dbname hintlist =
   let check (_, h) =
@@ -905,7 +940,7 @@ type hint_obj = {
 let load_autohint _ (kn, h) =
   let name = h.hint_name in
   match h.hint_action with
-  | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b)
+  | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty ~name st b)
   | AddTransparency (grs, b) -> add_transparency name grs b
   | AddHints hints -> add_hint name hints
   | RemoveHints grs -> remove_hint name grs
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 6f5ee8ba5e..411540aa1b 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -43,11 +43,14 @@ type hints_path_atom =
   (* For forward hints, their names is the list of projections *)
   | PathAny
 
+type hint_db_name = string
+
 type 'a with_metadata = private {
   pri   : int;            (** A number between 0 and 4, 4 = lower priority *)
   poly  : polymorphic;    (** Is the hint polymorpic and hence should be refreshed at each application *)
   pat   : constr_pattern option; (** A pattern for the concl of the Goal *)
   name  : hints_path_atom; (** A potential name to refer to the hint *) 
+  db    : hint_db_name option;
   code  : 'a; (** the tactic to apply when the concl matches pat *)
 }
 
@@ -77,7 +80,7 @@ val pp_hint_mode : hint_mode -> Pp.std_ppcmds
 module Hint_db :
   sig
     type t
-    val empty : transparent_state -> bool -> t
+    val empty : ?name:hint_db_name -> transparent_state -> bool -> t
     val find : global_reference -> t -> search_entry
     val map_none : t -> full_hint list
 
@@ -113,8 +116,6 @@ module Hint_db :
     val unfolds : t -> Id.Set.t * Cset.t
   end
 
-type hint_db_name = string
-
 type hint_db = Hint_db.t
 
 type hnf = bool
-- 
cgit v1.2.3


From 5232d2a29506ee30bf54336acf9998684a3b1cd9 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 6 Oct 2016 18:54:21 +0200
Subject: Fix git recognition when in worktrees.

git worktrees have a .git file instead of a .git directory.
Using Sys.file_exists is a more general solution which gives true in both cases.
---
 configure.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/configure.ml b/configure.ml
index 23ec93e078..507fd351a7 100644
--- a/configure.ml
+++ b/configure.ml
@@ -430,7 +430,7 @@ let dll = if os_type_win32 then ".dll" else ".so"
 
 let vcs =
   let git_dir = try Sys.getenv "GIT_DIR" with Not_found -> ".git" in
-  if dir_exists git_dir then "git"
+  if Sys.file_exists git_dir then "git"
   else if Sys.file_exists ".svn/entries" then "svn"
   else if dir_exists "{arch}" then "gnuarch"
   else "none"
-- 
cgit v1.2.3


From 472914e8844387b756305eff0720fc8acb345d45 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 12 Oct 2016 14:09:20 +0200
Subject: Fix bug #5116: [Print Ltac] should be able to print strategies.

---
 ltac/g_rewrite.ml4 | 13 +++++++++++--
 ltac/rewrite.ml    | 34 ++++++++++++++++++++++++++++++++++
 ltac/rewrite.mli   |  3 +++
 3 files changed, 48 insertions(+), 2 deletions(-)

diff --git a/ltac/g_rewrite.ml4 b/ltac/g_rewrite.ml4
index 82b79c883d..28078efd64 100644
--- a/ltac/g_rewrite.ml4
+++ b/ltac/g_rewrite.ml4
@@ -63,8 +63,17 @@ let glob_strategy ist s = map_strategy (Tacintern.intern_constr ist) (fun c -> c
 let subst_strategy s str = str
 
 let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>"
-let pr_raw_strategy _ _ _ (s : raw_strategy) = Pp.str "<strategy>"
-let pr_glob_strategy _ _ _ (s : glob_strategy) = Pp.str "<strategy>"
+let pr_raw_strategy prc prlc _ (s : raw_strategy) =
+  let prr = Pptactic.pr_red_expr (prc, prlc, Pptactic.pr_or_by_notation Libnames.pr_reference, prc) in
+  Rewrite.pr_strategy prc prr s
+let pr_glob_strategy prc prlc _ (s : glob_strategy) =
+  let prr = Pptactic.pr_red_expr
+    (Ppconstr.pr_constr_expr,
+    Ppconstr.pr_lconstr_expr,
+    Pptactic.pr_or_by_notation Libnames.pr_reference,
+    Ppconstr.pr_constr_expr)
+  in
+  Rewrite.pr_strategy prc prr s
 
 ARGUMENT EXTEND rewstrategy
     PRINTED BY pr_strategy
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 69f45e1aeb..4d7c5d0e4b 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1700,6 +1700,40 @@ let rec map_strategy (f : 'a -> 'a2) (g : 'b -> 'b2) : ('a,'b) strategy_ast -> (
   | StratEval r -> StratEval (g r)
   | StratFold c -> StratFold (f c)
 
+let pr_ustrategy = function
+| Subterms -> str "subterms"
+| Subterm -> str "subterm"
+| Innermost -> str "innermost"
+| Outermost -> str "outermost"
+| Bottomup -> str "bottomup"
+| Topdown -> str "topdown"
+| Progress -> str "progress"
+| Try -> str "try"
+| Any -> str "any"
+| Repeat -> str "repeat"
+
+let paren p = str "(" ++ p ++ str ")"
+
+let rec pr_strategy prc prr = function
+| StratId -> str "id"
+| StratFail -> str "fail"
+| StratRefl -> str "refl"
+| StratUnary (s, str) ->
+  pr_ustrategy s ++ spc () ++ paren (pr_strategy prc prr str)
+| StratBinary (Choice, str1, str2) ->
+  str "choice" ++ spc () ++ paren (pr_strategy prc prr str1) ++ spc () ++
+    paren (pr_strategy prc prr str2)
+| StratBinary (Compose, str1, str2) ->
+  pr_strategy prc prr str1 ++ str ";" ++ spc () ++ pr_strategy prc prr str2
+| StratConstr (c, true) -> prc c
+| StratConstr (c, false) -> str "<-" ++ spc () ++ prc c
+| StratTerms cl -> str "terms" ++ spc () ++ pr_sequence prc cl
+| StratHints (old, id) ->
+  let cmd = if old then "old_hints" else "hints" in
+  str cmd ++ spc () ++ str id
+| StratEval r -> str "eval" ++ spc () ++ prr r
+| StratFold c -> str "fold" ++ spc () ++ prc c
+
 let rec strategy_of_ast = function
   | StratId -> Strategies.id
   | StratFail -> Strategies.fail
diff --git a/ltac/rewrite.mli b/ltac/rewrite.mli
index f448c85430..35c4483513 100644
--- a/ltac/rewrite.mli
+++ b/ltac/rewrite.mli
@@ -62,6 +62,9 @@ val strategy_of_ast : (glob_constr_and_expr, raw_red_expr) strategy_ast -> strat
 val map_strategy : ('a -> 'b) -> ('c -> 'd) ->
   ('a, 'c) strategy_ast -> ('b, 'd) strategy_ast
 
+val pr_strategy : ('a -> Pp.std_ppcmds) -> ('b -> Pp.std_ppcmds) ->
+  ('a, 'b) strategy_ast -> Pp.std_ppcmds
+
 (** Entry point for user-level "rewrite_strat" *)
 val cl_rewrite_clause_strat : strategy -> Id.t option -> unit Proofview.tactic
 
-- 
cgit v1.2.3


From 5dd690ee5975262d34d8dcc44191138c8d326f65 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 16 Jul 2016 16:24:59 +0200
Subject: Fixing a collision about the meta-variable ".." in recursive
 notations.

This happens when recursive notations are used to define recursive
notations.
---
 interp/constrintern.ml         | 20 ++++++++------------
 test-suite/success/Notations.v |  3 +++
 2 files changed, 11 insertions(+), 12 deletions(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f30d3cefad..478adf0115 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -517,27 +517,24 @@ let rec subordinate_letins letins = function
   | [] ->
       letins,[]
 
-let rec subst_iterator y t = function
-  | GVar (_,id) as x -> if Id.equal id y then t else x
-  | x -> map_glob_constr (subst_iterator y t) x
-
 let subst_aconstr_in_glob_constr loc intern (_,ntnvars as lvar) subst infos c =
   let (terms,termlists,binders) = subst in
   (* when called while defining a notation, avoid capturing the private binders
      of the expression by variables bound by the notation (see #3892) *)
   let avoid = Id.Map.domain ntnvars in
-  let rec aux (terms,binderopt as subst') (renaming,env) c =
+  let rec aux (terms,binderopt,terminopt as subst') (renaming,env) c =
     let subinfos = renaming,{env with tmp_scope = None} in
     match c with
+    | NVar id when Id.equal id ldots_var -> Option.get terminopt
     | NVar id -> subst_var subst' (renaming, env) id
     | NList (x,_,iter,terminator,lassoc) ->
       (try
         (* All elements of the list are in scopes (scopt,subscopes) *)
 	let (l,(scopt,subscopes)) = Id.Map.find x termlists in
-        let termin = aux subst' subinfos terminator in
+        let termin = aux (terms,None,None) subinfos terminator in
         let fold a t =
           let nterms = Id.Map.add x (a, (scopt, subscopes)) terms in
-          subst_iterator ldots_var t (aux (nterms, binderopt) subinfos iter)
+          aux (nterms,None,Some t) subinfos iter
         in
 	List.fold_right fold (if lassoc then List.rev l else l) termin
       with Not_found ->
@@ -582,10 +579,9 @@ let subst_aconstr_in_glob_constr loc intern (_,ntnvars as lvar) subst infos c =
 	let (bl,(scopt,subscopes)) = Id.Map.find x binders in
 	let env,bl = List.fold_left (intern_local_binder_aux intern lvar) (env,[]) bl in
 	let letins,bl = subordinate_letins [] bl in
-        let termin = aux subst' (renaming,env) terminator in
+        let termin = aux (terms,None,None) (renaming,env) terminator in
 	let res = List.fold_left (fun t binder ->
-          subst_iterator ldots_var t
-	    (aux (terms,Some(x,binder)) subinfos iter))
+	    aux (terms,Some(x,binder),Some t) subinfos iter)
 	  termin bl in
 	make_letins letins res
       with Not_found ->
@@ -610,7 +606,7 @@ let subst_aconstr_in_glob_constr loc intern (_,ntnvars as lvar) subst infos c =
     | t ->
       glob_constr_of_notation_constr_with_binders loc
         (traverse_binder subst avoid) (aux subst') subinfos t
-  and subst_var (terms, binderopt) (renaming, env) id =
+  and subst_var (terms, _binderopt, _terminopt) (renaming, env) id =
     (* subst remembers the delimiters stack in the interpretation *)
     (* of the notations *)
     try
@@ -623,7 +619,7 @@ let subst_aconstr_in_glob_constr loc intern (_,ntnvars as lvar) subst infos c =
     with Not_found ->
       (* Happens for local notation joint with inductive/fixpoint defs *)
       GVar (loc,id)
-  in aux (terms,None) infos c
+  in aux (terms,None,None) infos c
 
 let split_by_type ids =
   List.fold_right (fun (x,(scl,typ)) (l1,l2,l3) ->
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index b72a067407..2f7c62972a 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -107,3 +107,6 @@ Notation traverse_var f l := (traverse (fun l => f l) l).
 
 Notation "'intros' x" := (S x) (at level 0).
 Goal True -> True. intros H. exact H. Qed.
+
+(* Check absence of collision on ".." in nested notations with ".." *)
+Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)).
-- 
cgit v1.2.3


From 63ff356a8546fbcb883bb6a9711c785f75fecd41 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 12 Oct 2016 16:14:00 +0200
Subject: Little addition to 6eede071 for consistency of style in
 OrdersFacts.v.

---
 theories/Structures/OrdersFacts.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index 6f8fc1b324..0115d8a544 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -434,14 +434,14 @@ Lemma eqb_compare x y :
  (x =? y) = match compare x y with Eq => true | _ => false end.
 Proof.
 apply eq_true_iff_eq. rewrite eqb_eq, <- compare_eq_iff.
-destruct compare; now split.
+now destruct compare.
 Qed.
 
 Lemma ltb_compare x y :
  (x <? y) = match compare x y with Lt => true | _ => false end.
 Proof.
 apply eq_true_iff_eq. rewrite ltb_lt, <- compare_lt_iff.
-destruct compare; now split.
+now destruct compare.
 Qed.
 
 Lemma leb_compare x y :
-- 
cgit v1.2.3


From 8b2a08ecd123515778584596918666e5f49076f7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 12 Oct 2016 17:08:11 +0200
Subject: Tentatively preparing to add changes specific to v8.7 (see PR #275).

---
 CHANGES | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/CHANGES b/CHANGES
index 0210281c3a..0b710c72f6 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,5 +1,5 @@
-Changes beyond V8.5
-===================
+Changes from V8.5 to V8.6beta1
+==============================
 
 Bugfixes
 
-- 
cgit v1.2.3