diff options
| author | Emilio Jesus Gallego Arias | 2020-03-09 01:51:37 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 06:03:42 -0400 |
| commit | 09d6197bd11ed4a323b335118ae749d7caefeb55 (patch) | |
| tree | 361c538ea06c34e8e1dc99309fa62816bb759e01 /vernac/declareDef.ml | |
| parent | a0296d51711cdd42f201b9d0e937266984a20944 (diff) | |
[proof] [mutual] Factorize notation declaration.
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 = |