From 56744aadd413dd9417d245951083117b05170e14 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 22 Oct 2016 11:38:51 +0200
Subject: Fixing printing of generic arguments of tag "var".

---
 tactics/tacinterp.ml       | 3 +++
 test-suite/output/ltac.out | 1 +
 test-suite/output/ltac.v   | 5 +++++
 3 files changed, 9 insertions(+)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 5ecc46d670..c3f7fa1439 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -816,6 +816,9 @@ let rec message_of_value v =
       Ftactic.return (pr_closed_glob_env (pf_env gl)
                         (Proofview.Goal.sigma gl) c)
     end
+  else if has_type v (topwit wit_var) then
+    let id = out_gen (topwit wit_var) v in
+    Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_id id) end
   else match Value.to_list v with
   | Some l ->
     Ftactic.List.map message_of_value l >>= fun l ->
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index d003c70df9..266e4c7243 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -1,2 +1,3 @@
 The command has indeed failed with message:
 Error: Ltac variable y depends on pattern variable name z which is not bound in current context.
+Hx
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 7e2610c7d7..e5bcff8ddb 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -15,3 +15,8 @@ lazymatch goal with
 | H1 : HT |- _ => idtac
 end.
 Abort.
+
+(* Check printing of the "var" argument "Hx" *)
+Ltac m H := idtac H; exact H.
+Goal True.
+let a:=constr:(let Hx := 0 in ltac:(m Hx)) in idtac.
-- 
cgit v1.2.3


From 9f8714f4cd3fb59ce38afee48caf081db1919c0c Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 5 Oct 2016 08:22:57 +0200
Subject: Fix incorrect token description for bullets.

---
 parsing/tok.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/parsing/tok.ml b/parsing/tok.ml
index c96b53de41..25633c63d0 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -55,7 +55,7 @@ let to_string = function
   | INT s -> Format.sprintf "INT %s" s
   | STRING s -> Format.sprintf "STRING %S" s
   | LEFTQMARK -> "LEFTQMARK"
-  | BULLET s -> Format.sprintf "STRING %S" s
+  | BULLET s -> Format.sprintf "BULLET %S" s
   | EOI -> "EOI"
 
 let match_keyword kwd = function
-- 
cgit v1.2.3


From cc2778c3310a75585c00f0eb659ddde7aee2944a Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 28 Sep 2016 17:00:09 +0200
Subject: Do not stop propagation of signals when Coq is busy (bug #3941).

When inserting a character in an already processed buffer, a message is
sent to Coq so that the proof is backtracked and the character is
inserted. If a second character is inserted while Coq is still busy with
the first message, the action is canceled, but the signal is no longer
dropped so that the second character is properly inserted.
---
 ide/session.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/ide/session.ml b/ide/session.ml
index 168ddd4df9..711111139e 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -111,10 +111,10 @@ let set_buffer_handlers
     let id = ref 0 in
     fun () -> incr id; !id in
   let running_action = ref None in
-  let cancel_signal reason =
+  let cancel_signal ?(stop_emit=true) reason =
     Minilib.log ("user_action cancelled: "^reason);
     action_was_cancelled := true;
-    GtkSignal.stop_emit () in
+    if stop_emit then GtkSignal.stop_emit () in
   let del_mark () =
     try buffer#delete_mark (`NAME "target")
     with GText.No_such_mark _ -> () in
@@ -127,7 +127,7 @@ let set_buffer_handlers
       fun () -> (* If Coq is busy due to the current action, we don't cancel *)
         match !running_action with
         | Some aid when aid = action -> ()
-        | _ -> cancel_signal "Coq busy" in
+        | _ -> cancel_signal ~stop_emit:false "Coq busy" in
     Coq.try_grab coqtop action fallback in
   let get_start () = buffer#get_iter_at_mark (`NAME "start_of_input") in
   let get_stop () = buffer#get_iter_at_mark (`NAME "stop_of_input") in
-- 
cgit v1.2.3


From 80d5779409bf33fbe5043275b96775a5f04a3b2c Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 28 Sep 2016 15:38:33 +0200
Subject: Remove incorrect assertion in cbn (bug #4822).

This assertion checked that two arguments in the same position were equal,
but in fact, since one might have already been reduced, they are only
convertible (which is too costly to check in an assertion).
---
 pretyping/reductionops.ml | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 7c7b31395e..9e654d29a1 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -153,9 +153,6 @@ module Cst_stack = struct
   let empty = []
   let is_empty = CList.is_empty
 
-  let sanity x y =
-    assert(Term.eq_constr x y)
-
   let drop_useless = function
     | _ :: ((_,_,[])::_ as q) -> q
     | l -> l
@@ -164,9 +161,9 @@ module Cst_stack = struct
     let append2cst = function
       | (c,params,[]) -> (c, h::params, [])
       | (c,params,((i,t)::q)) when i = pred (Array.length t) ->
-	 let () = sanity h t.(i) in (c, params, q)
+	(c, params, q)
       | (c,params,(i,t)::q) ->
-	let () = sanity h t.(i) in (c, params, (succ i,t)::q)
+	(c, params, (succ i,t)::q)
     in
       drop_useless (List.map append2cst cst_l)
 
-- 
cgit v1.2.3