Local universes for opaque polymorphic constants.

1 files changed, 1 insertions, 1 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 1cf952576d..5ba9735690 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -322,7 +322,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
     (* 	end; *)
 
       let open Proof_global in
-      let { id; entries; persistence } = fst @@ close_proof ~keep_body_ucst_separate:false (fun x -> x) in
+      let { id; entries; persistence } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) in
       match entries with
       | [entry] ->
         discard_current ();