Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).

This allows e.g. the following to work:

Reserved Notation "* a" (at level 70).
Inductive P {n : nat} : nat -> Prop := c m : *m where "* m" := (P m).

We seize this opportunity to make main calls to Metasyntax to depend
on an arbitrary env rather than on Global.env.

Incidentally, this fixes a little coqdoc bug in classifying the
inductive type referred to in the "where" clause.

1 files changed, 28 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/5762.v b/test-suite/bugs/closed/5762.v
new file mode 100644
index 0000000000..edd5c8d73d
--- /dev/null
+++ b/test-suite/bugs/closed/5762.v
@@ -0,0 +1,28 @@
+(* Supporting imp. params. in inductive or fixpoints mutually defined with a notation *)
+
+Reserved Notation "* a" (at level 70).
+Inductive P {n : nat} : nat -> Prop :=
+| c m : *m
+where "* m" := (P m).
+
+Reserved Notation "##".
+Inductive I {A:Type} := C : ## where "##" := I.
+
+(* The following was working in 8.6 *)
+
+Require Import Vector.
+
+Reserved Notation "# a" (at level 70).
+Fixpoint f {n : nat} (v:Vector.t nat n) : nat :=
+  match v with
+  | nil _ => 0
+  | cons _ _ _ v => S (#v)
+  end
+where "# v" := (f v).
+
+(* The following was working in 8.6 *)
+
+Reserved Notation "%% a" (at level 70).
+Record R :=
+  {g : forall {A} (a:A), a=a where "%% x" := (g x);
+   k : %% 0 = eq_refl}.