diff options
| author | Hugo Herbelin | 2017-04-06 11:15:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-04-06 11:28:08 +0200 |
| commit | 33f40197e6b7bef02c8df2dc0a0066f8144b66d6 (patch) | |
| tree | 1ed61e9efe45f04b9f03229eec2ad986dde02059 /toplevel | |
| parent | c6f24b1cbfb485dbf14b3934208c113140de2eca (diff) | |
| parent | ed25677029e2cc1e34eba76aade1a00980ca11de (diff) | |
Merge branch 'origin/v8.5' into v8.6.
Was needed to be done for a while.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index a9f2598e22..93f156ee2b 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -591,12 +591,13 @@ let interp_mutual_inductive (paramsl,indl) notations 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 (Inductive params) indnames fullarities indimpls in + let implsforntn = compute_internalization_env env0 Variable 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 impls) notations; + List.iter (Metasyntax.set_notation_for_interpretation implsforntn) notations; (* Interpret the constructor types *) List.map3 (interp_cstrs env_ar_params evdref impls) mldatas arities indl) () in |