diff options
| -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 |