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/declareDef.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/declareDef.ml')
| -rw-r--r-- | vernac/declareDef.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index dea2ccb9af..39fd332184 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -69,11 +69,6 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = end; dref -let declare_fix ?(opaque = false) ?hook_data ~name ~scope ~kind udecl univs ((def,_),eff) t imps = - let ce = definition_entry ~opaque ~types:t ~univs ~eff def in - let kind = Decls.IsDefinition kind in - declare_definition ~name ~scope ~kind ?hook_data udecl ce imps - let warn_let_as_axiom = CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++ |