Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 (clause "where" with implicit arguments)

6 files changed, 28 insertions, 11 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c4e0ac500c..dee415f8f7 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/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out
index 70cbe50657..5e4b676c2f 100644
--- a/test-suite/coqdoc/links.html.out
+++ b/test-suite/coqdoc/links.html.out
@@ -76,7 +76,7 @@ Various checks for coqdoc
 <br/>
 <span class="id" title="keyword">Inductive</span> <a name="eq"><span class="id" title="inductive">eq</span></a> (<span class="id" title="var">A</span>:<span class="id" title="keyword">Type</span>) (<span class="id" title="var">x</span>:<a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a>) : <span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> := <a name="eq_refl"><span class="id" title="constructor">eq_refl</span></a> : <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:&gt;</span></a><a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a><br/>
 <br/>
-<span class="id" title="keyword">where</span> <a name="8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">&quot;</span></a>x = y :&gt; A" := (@<a class="idref" href="Coqdoc.links.html#eq"><span class="id" title="inductive">eq</span></a> <a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/>
+<span class="id" title="keyword">where</span> <a name="8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">&quot;</span></a>x = y :&gt; A" := (@<a class="idref" href="Coqdoc.links.html#eq"><span class="id" title="inductive">eq</span></a> <span class="id" title="var">A</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/>
 
 <br/>
 <span class="id" title="keyword">Definition</span> <a name="eq0"><span class="id" title="definition">eq0</span></a> := 0 <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:&gt;</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/>
diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out
index 7d93189ae2..f42db99dc2 100644
--- a/test-suite/coqdoc/links.tex.out
+++ b/test-suite/coqdoc/links.tex.out
@@ -69,7 +69,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/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).
diff --git a/vernac/command.ml b/vernac/command.ml
index be54f97b72..b027863e8e 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -551,12 +551,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