From 8fbc927ac40cc707b1a940d8339a2a289755d533 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 14 Mar 2020 16:34:30 -0400
Subject: [declareDef] More consistent handling of universe binders

The only reasons that `prepare_definition` returned a sigma were:
- to obtain the universe binders to be passed to declare
- to obtain the UState.t to be passed to the equations hook

We handle this automatically now; it seems like a reasonably good API
improvement.

However, it is not clear what we do now is right for all cases; must
check.
---
 plugins/funind/gen_principle.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 47e56b81aa..ebd280ecf6 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -290,13 +290,11 @@ let generate_functional_principle (evd: Evd.evar_map ref)
      Don't forget to close the goal if an error is raised !!!!
   *)
   let uctx = Evd.evar_universe_context sigma in
-  let hook_data = hook, uctx, [] in
-  let entry = DeclareDef.ClosedDef.of_proof_entry entry in
+  let entry = DeclareDef.ClosedDef.of_proof_entry ~uctx entry in
   let _ : Names.GlobRef.t = DeclareDef.declare_definition
-      ~name:new_princ_name ~hook_data
+      ~name:new_princ_name ~hook
       ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
       ~kind:Decls.(IsProof Theorem)
-      ~ubind:UnivNames.empty_binders
       ~impargs:[]
       entry in
   ()
-- 
cgit v1.2.3