aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/pfedit.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/pfedit.ml')
-rw-r--r--proofs/pfedit.ml6
1 files changed, 2 insertions, 4 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 193788558..23f96b5a3 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -239,7 +239,6 @@ let get_current_proof_name = Proof_global.get_current_proof_name
let get_all_proof_names = Proof_global.get_all_proof_names
type lemma_possible_guards = Proof_global.lemma_possible_guards
-type universe_binders = Proof_global.universe_binders
let delete_proof = Proof_global.discard
let delete_current_proof = Proof_global.discard_current
@@ -257,6 +256,5 @@ let set_used_variables l =
let get_used_variables () =
Proof_global.get_used_variables ()
-let get_universe_binders () =
- Proof_global.get_universe_binders ()
-
+let get_universe_decl () =
+ Proof_global.get_universe_decl ()