diff options
| author | Emilio Jesus Gallego Arias | 2020-04-18 23:21:05 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-21 08:39:13 +0200 |
| commit | 579d192cc4c21d3a2a325dc501181d262040482f (patch) | |
| tree | ea096cf2a678547d1876ec5f9c90c913bfd61eb4 /vernac/indschemes.ml | |
| parent | 77fc6ad50fb2bd95d19ecaee36fa34c7931a2bc1 (diff) | |
[nit] Remove useless indirect alias.
Diffstat (limited to 'vernac/indschemes.ml')
| -rw-r--r-- | vernac/indschemes.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 7260b13ff6..6ffa88874b 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -91,12 +91,11 @@ let () = optwrite = (fun b -> rewriting_flag := b) } (* Util *) - let define ~poly name sigma c types = - let f = declare_constant ~kind:Decls.(IsDefinition Scheme) in let univs = Evd.univ_entry ~poly sigma in let entry = Declare.definition_entry ~univs ?types c in - let kn = f ~name (DefinitionEntry entry) in + let kind = Decls.(IsDefinition Scheme) in + let kn = declare_constant ~kind ~name (DefinitionEntry entry) in definition_message name; kn |
