Merge branch 'origin/v8.5' into v8.6.

Was needed to be done for a while.

4 files changed, 17 insertions, 7 deletions

diff --git a/ltac/tactic_debug.ml b/ltac/tactic_debug.ml
index 5cbddc7f64..698c913e84 100644
--- a/ltac/tactic_debug.ml
+++ b/ltac/tactic_debug.ml
@@ -108,6 +108,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
@@ -118,14 +120,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 =
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 52acad7460..837f2efd06 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -121,6 +121,7 @@ Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10).
 Goal True.
 {{ exact I. }}
 Qed.
+
 Check |- {{ 0 }} 0.
 
 (* Check parsing of { and } is not affected by notations #3479 *)
@@ -135,3 +136,9 @@ Notation "" := (@nil) (only printing).
 
 (* Check that a notation cannot be neither parsing nor printing. *)
 Fail Notation "'foobarkeyword'" := (@nil) (only parsing, only printing).
+
+(* 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/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 *)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index a9f2598e22..93f156ee2b 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -591,12 +591,13 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
     lift_implicits (Context.Rel.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