From fedc831df9626a31cd0d26ee6b9e022b67f90c2a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 23 Feb 2017 14:34:44 +0100
Subject: Fixing a little bug in using the "where" clause for inductive types.

This was not working when the inductive type had implicit parameters.

This could still be improved. E.g. the following still does not work:

Reserved Notation "#".
Inductive I {A:Type} := C : # where "#" := I.

But it should be made working by taking care of adding the mandatory
implicit argument A at the time # is interpreted as [@I _]
(i.e., technically speaking, using expl_impls in interp_notation).
---
 test-suite/success/Notations.v | 6 ++++++
 toplevel/command.ml            | 3 ++-
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 511b60b4bb..8c83b196e4 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -116,3 +116,9 @@ Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10).
 Goal True.
 {{ exact I. }}
 Qed.
+
+(* Check "where" clause for inductive types with parameters *)
+
+Reserved Notation "x === y" (at level 50).
+Inductive EQ {A} (x:A) : A -> Prop := REFL : x === x
+ where "x === y" := (EQ x y).
diff --git a/toplevel/command.ml b/toplevel/command.ml
index b9e4dbd7b2..8926b410c6 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -571,12 +571,13 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
     lift_implicits (rel_context_nhyps ctx_params) impls) arities in
   let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in
   let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in
+  let implsforntn = compute_internalization_env env0 Variable indnames fullarities indimpls in
   let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
 
   let constructors =
     Metasyntax.with_syntax_protection (fun () ->
      (* Temporary declaration of notations and scopes *)
-     List.iter (Metasyntax.set_notation_for_interpretation impls) notations;
+     List.iter (Metasyntax.set_notation_for_interpretation implsforntn) notations;
      (* Interpret the constructor types *)
      List.map3 (interp_cstrs env_ar_params evdref impls) mldatas arities indl)
      () in
-- 
cgit v1.2.3


From 8451b4ae99b448894a6269c08be7f3ac0d74cac4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 23 Feb 2017 14:58:17 +0100
Subject: Fixing a little bug in printing ex2 (type was printed "_" by
 default).

---
 theories/Init/Logic.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 85123cc444..b32985b800 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -243,9 +243,9 @@ Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..))
 
 Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q))
   (at level 200, x ident, p at level 200, right associativity) : type_scope.
-Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q))
-  (at level 200, x ident, t at level 200, p at level 200, right associativity,
-    format "'[' 'exists2'  '/  ' x  :  t ,  '/  ' '[' p  &  '/' q ']' ']'")
+Notation "'exists2' x : A , p & q" := (ex2 (A:=A) (fun x => p) (fun x => q))
+  (at level 200, x ident, A at level 200, p at level 200, right associativity,
+    format "'[' 'exists2'  '/  ' x  :  A ,  '/  ' '[' p  &  '/' q ']' ']'")
   : type_scope.
 
 (** Derived rules for universal quantification *)
-- 
cgit v1.2.3


From ed25677029e2cc1e34eba76aade1a00980ca11de Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 24 Feb 2017 09:39:50 +0100
Subject: Fixing anomaly on unsupported key in interactive ltac debug.

---
 proofs/tactic_debug.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index a4a447e88f..6aae6e98bb 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -98,6 +98,8 @@ let string_get s i =
   try Proofview.NonLogical.return (String.get s i)
   with e -> Proofview.NonLogical.raise e
 
+let run_invalid_arg () = Proofview.NonLogical.raise (Invalid_argument "run_com")
+
 (* Gives the number of steps or next breakpoint of a run command *)
 let run_com inst =
   let open Proofview.NonLogical in
@@ -108,14 +110,14 @@ let run_com inst =
       let s = String.sub inst i (String.length inst - i) in
       if inst.[0] >= '0' && inst.[0] <= '9' then
         int_of_string s >>= fun num ->
-        (if num<0 then invalid_arg "run_com" else return ()) >>
+        (if num<0 then run_invalid_arg () else return ()) >>
         (skip:=num) >> (skipped:=0)
       else
         breakpoint:=Some (possibly_unquote s)
     else
-      invalid_arg "run_com"
+      run_invalid_arg ()
   else
-    invalid_arg "run_com"
+    run_invalid_arg ()
 
 (* Prints the run counter *)
 let run ini =
-- 
cgit v1.2.3