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/comFixpoint.ml | |
| parent | a0296d51711cdd42f201b9d0e937266984a20944 (diff) | |
[proof] [mutual] Factorize notation declaration.
Diffstat (limited to 'vernac/comFixpoint.ml')
| -rw-r--r-- | vernac/comFixpoint.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 55ef0f67d6..ced9656218 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -282,10 +282,9 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt let univs = Evd.check_univ_decl ~poly evd pl in let ubind = Evd.universe_binders evd in let _ : GlobRef.t list = - DeclareDef.declare_mutually_recursive ~indexes ~cofix ~scope ~opaque:false ~univs ~kind:fix_kind ~ubind + DeclareDef.declare_mutually_recursive ~indexes ~cofix ~scope ~opaque:false ~univs ~kind:fix_kind ~ubind ~ntns fixnames fixdecls fixtypes fiximps in - List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; () let extract_decreasing_argument ~structonly { CAst.v = v; _ } = |