From 5f937b2f8532b2ccf36c62557934cc2c9150005b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 9 Mar 2020 06:32:00 -0400
Subject: [proof] Miscellaneous cleanup on proof info handling

After the refactorings proof information is organized in a slightly
different way thus the lower layers don't need to pass info back
anymore.
---
 plugins/funind/gen_principle.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 446026c4c8..28cf5c7d98 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -199,7 +199,7 @@ let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_
   (*    end; *)
 
   let open Proof_global in
-  let { name; entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)) lemma in
+  let { entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)) lemma in
   match entries with
   | [entry] ->
     entry, hook
-- 
cgit v1.2.3