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.]
---
 vernac/command.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'vernac')

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