From ac76f1f2bf819a5999cef642f17652320f39fd80 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 8 Nov 2017 18:40:14 +0100
Subject: Fixing a remaining "coqdoc" problem with bug #5762 and pr #1120.
PR #1120 was still buggy for the following reasons: variables in the
lhs of the notation were linked in the glob file while they have
nowhere to link to (the binder is the notation string) [I thought the
change I commited in links.html.out was actually improving but it was
an overlook, sorry.]
---
test-suite/coqdoc/links.html.out | 2 +-
test-suite/coqdoc/links.tex.out | 2 +-
vernac/command.ml | 3 ++-
3 files changed, 4 insertions(+), 3 deletions(-)
diff --git a/test-suite/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out
index e2928f78d4..a492905ed8 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 de3182d1a0..235c287b5f 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" := (@\coqref{Coqdoc.links.eq}{\coqdocinductive{eq}} \coqdocvariable{A} \coqdocvariable{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}} \coqdocvar{A} \coqdocvar{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
diff --git a/vernac/command.ml b/vernac/command.ml
index f58ed065c6..6567767271 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -550,12 +550,13 @@ let interp_mutual_inductive (paramsl,indl) notations cum 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 ~impls (Inductive (params,true)) indnames fullarities indimpls in
+ let ntn_impls = compute_internalization_env env0 (Inductive (params,true)) 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 env_params impls) notations;
+ List.iter (Metasyntax.set_notation_for_interpretation env_params ntn_impls) notations;
(* Interpret the constructor types *)
List.map3 (interp_cstrs env_ar_params evdref impls) mldatas arities indl)
() in
--
cgit v1.2.3
From 685643098eeef00fe1f8dfca0927db2e812e1e7a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 8 Nov 2017 19:58:41 +0100
Subject: One more step in fixing #5762 ("where" clause).
We improve one step further the heuristics to sort out if a variable
is a notation variable or a named variable.
This allows to support the following which was still failing.
Reserved Notation "# x" (at level 0).
Inductive I {A:Type} := C : # 0 -> I where "# I" := (I = I).
We rely here on the property that a binding variable of same name as a
notation variables is itself considered bound by the notation.
This becomes however to be a bit tricky for sorting out if the
variable has to be output to the glob file or not.
---
interp/constrintern.ml | 20 ++++++++++++--------
test-suite/bugs/closed/5762.v | 6 ++++++
test-suite/success/Notations2.v | 6 ++++++
3 files changed, 24 insertions(+), 8 deletions(-)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index a0a749bfb3..e20a159f89 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -534,8 +534,9 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function
| Name id ->
try
(* Binders bound in the notation are considered first-order objects *)
- let _,na = coerce_to_name (fst (Id.Map.find id terms)) in
- (renaming,{env with ids = Name.fold_right Id.Set.add na env.ids}), na
+ let _,na as locna = coerce_to_name (fst (Id.Map.find id terms)) in
+ let env = push_name_env Id.Map.empty (Variable,[],[],[]) env locna in
+ (renaming,env), na
with Not_found ->
(* Binders not bound in the notation do not capture variables *)
(* outside the notation (i.e. in the substitution) *)
@@ -747,7 +748,14 @@ let gvar (loc, id) us = match us with
str " cannot have a universe instance")
let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
- (* Is [id] an inductive type potentially with implicit *)
+ (* Is [id] a notation variable *)
+ if Id.Map.mem id ntnvars then
+ begin
+ if not (Id.Map.mem id genv.impls) then set_var_scope ?loc id true genv ntnvars;
+ gvar (loc,id) us, [], [], []
+ end
+ else
+ (* Is [id] registered with implicit arguments *)
try
let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in
let expl_impls = List.map
@@ -760,12 +768,8 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
if Id.Set.mem id genv.ids || Id.Set.mem id ltacvars.ltac_vars
then
gvar (loc,id) us, [], [], []
- (* Is [id] a notation variable *)
- else if Id.Map.mem id ntnvars
- then
- (set_var_scope ?loc id true genv ntnvars; gvar (loc,id) us, [], [], [])
- (* Is [id] the special variable for recursive notations *)
else if Id.equal id ldots_var
+ (* Is [id] the special variable for recursive notations? *)
then if Id.Map.is_empty ntnvars
then error_ldots_var ?loc
else gvar (loc,id) us, [], [], []
diff --git a/test-suite/bugs/closed/5762.v b/test-suite/bugs/closed/5762.v
index edd5c8d73d..55d36bd722 100644
--- a/test-suite/bugs/closed/5762.v
+++ b/test-suite/bugs/closed/5762.v
@@ -26,3 +26,9 @@ Reserved Notation "%% a" (at level 70).
Record R :=
{g : forall {A} (a:A), a=a where "%% x" := (g x);
k : %% 0 = eq_refl}.
+
+(* An extra example *)
+
+Module A.
+Inductive I {A:Type} := C : # 0 -> I where "# I" := (I = I) : I_scope.
+End A.
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index 9505a56e3f..e86b3edb83 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -90,3 +90,9 @@ Check fun A (x :prod' bool A) => match x with #### 0 y 0 => 2 | _ => 1 end.
Notation "##### x" := (pair' x) (at level 0, x at level 1).
Check ##### 0 _ 0%bool 0%bool : prod' bool bool.
Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end.
+
+(* 10. Check computation of binding variable through other notations *)
+(* i should be detected as binding variable and the scopes not being checked *)
+
+Notation "'FUNNAT' i => t" := (fun i : nat => i = t) (at level 200).
+Notation "'Funnat' i => t" := (FUNNAT i => t + i%nat) (at level 200).
--
cgit v1.2.3