From 26f216653aed171a70513d3f5ece059ab30bcd73 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 4 Oct 2017 23:55:54 +0200
Subject: 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.
---
test-suite/bugs/closed/5762.v | 28 ++++++++++++++++++++++++++++
test-suite/coqdoc/links.html.out | 2 +-
test-suite/coqdoc/links.tex.out | 2 +-
3 files changed, 30 insertions(+), 2 deletions(-)
create mode 100644 test-suite/bugs/closed/5762.v
(limited to 'test-suite')
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}.
diff --git a/test-suite/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out
index 7d7d01c1b4..e2928f78d4 100644
--- a/test-suite/coqdoc/links.html.out
+++ b/test-suite/coqdoc/links.html.out
@@ -76,7 +76,7 @@ Various checks for coqdoc
Inductive eq (A:Type) (x:A) : A -> Prop := eq_refl : x = x :>A
-where "x = y :> A" := (@eq A x y) : type_scope.
+where "x = y :> A" := (@eq A x y) : type_scope.
Definition eq0 := 0 = 0 :> nat.
diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out
index 844fb3031c..de3182d1a0 100644
--- a/test-suite/coqdoc/links.tex.out
+++ b/test-suite/coqdoc/links.tex.out
@@ -59,7 +59,7 @@ Various checks for coqdoc
\coqdocnoindent
\coqdoceol
\coqdocnoindent
-\coqdockw{where} \coqdef{Coqdoc.links.:type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqdocvariable{eq} \coqdocvar{A} \coqdocvar{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol
+\coqdockw{where} \coqdef{Coqdoc.links.:type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqref{Coqdoc.links.eq}{\coqdocinductive{eq}} \coqdocvariable{A} \coqdocvariable{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Definition} \coqdef{Coqdoc.links.eq0}{eq0}{\coqdocdefinition{eq0}} := 0 \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{=}} 0 \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{:>}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol
--
cgit v1.2.3