diff options
| author | Emilio Jesus Gallego Arias | 2020-03-02 00:46:23 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-12 20:36:36 -0400 |
| commit | b35dae7a6a9cc08c4bcdce7409e0ef45382b7ee1 (patch) | |
| tree | 63f883491774712cd0ee267eee8f1d01b884e7a9 /vernac/comFixpoint.ml | |
| parent | 79bcf1c0a22e736c4e2cae3460c35b3d9fca9aa0 (diff) | |
[declare] Remove trivial wrapper
In preparation for the introduction of an opaque mutual definition
type at the `Declare` level we remove the not very useful wrapper
`declare_fix`.
Now we should be ready to profit from `DeclareDef` and its handling of
common stuff such as `restrict_universe_context` and `check_univ_decl`
etc...
Diffstat (limited to 'vernac/comFixpoint.ml')
| -rw-r--r-- | vernac/comFixpoint.ml | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index a29d60ccde..65dffb3c0b 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -272,8 +272,8 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = let indexes, cofix, fix_kind = match indexes with - | Some indexes -> indexes, false, Decls.Fixpoint - | None -> [], true, Decls.CoFixpoint + | Some indexes -> indexes, false, Decls.(IsDefinition Fixpoint) + | None -> [], true, Decls.(IsDefinition CoFixpoint) in (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in @@ -294,11 +294,13 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in let ctx = Evd.check_univ_decl ~poly evd pl in - let pl = Evd.universe_binders evd in - let mk_pure c = (c, Univ.ContextSet.empty), Evd.empty_side_effects in - let fixdecls = List.map mk_pure fixdecls in - ignore (List.map4 (fun name -> DeclareDef.declare_fix ~name ~scope ~kind:fix_kind pl ctx) - fixnames fixdecls fixtypes fiximps); + let udecl = Evd.universe_binders evd in + let _ : GlobRef.t list = + List.map4 (fun name body types imps -> + let ce = Declare.definition_entry ~opaque:false ~types ~univs:ctx body in + DeclareDef.declare_definition ~name ~scope ~kind:fix_kind udecl ce imps) + fixnames fixdecls fixtypes fiximps + in recursive_message (not cofix) gidx fixnames; List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; () |