diff options
Diffstat (limited to 'vernac/declareDef.ml')
| -rw-r--r-- | vernac/declareDef.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 9708f43e53..b3bcf58b4a 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -69,7 +69,7 @@ let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce = end; dref -let declare_mutually_recursive ~cofix ~indexes ~opaque ~univs ~scope ~kind ~ubind fixnames fixdecls fixtypes fiximps = +let declare_mutually_recursive ~cofix ~indexes ~opaque ~univs ~scope ~kind ~ubind ~ntns fixnames fixdecls fixtypes fiximps = let csts = CList.map4 (fun name body types impargs -> let ce = Declare.definition_entry ~opaque ~types ~univs body in @@ -77,6 +77,7 @@ let declare_mutually_recursive ~cofix ~indexes ~opaque ~univs ~scope ~kind ~ubin fixnames fixdecls fixtypes fiximps in Declare.recursive_message (not cofix) indexes fixnames; + List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; csts let warn_let_as_axiom = |