diff options
| author | Hugo Herbelin | 2017-11-08 18:40:14 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-11-08 19:36:10 +0100 |
| commit | ac76f1f2bf819a5999cef642f17652320f39fd80 (patch) | |
| tree | 82b9722b4067e9f89551409690f8d978cae5679f /vernac | |
| parent | 0d81e80a09db7d352408be4dfc5ba263f6ed98ef (diff) | |
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.]
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/command.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 |