From 579d192cc4c21d3a2a325dc501181d262040482f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 18 Apr 2020 23:21:05 -0400
Subject: [nit] Remove useless indirect alias.

---
 vernac/indschemes.ml | 5 ++---
 1 file 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
 
-- 
cgit v1.2.3