aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/goal.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/goal.ml')
-rw-r--r--proofs/goal.ml5
1 files changed, 0 insertions, 5 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml
index a2efc10f0..6cd00c318 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -466,11 +466,6 @@ module V82 = struct
let evi = content evars gl in
Evd.evar_filtered_env evi
- (* For printing *)
- let unfiltered_env evars gl =
- let evi = content evars gl in
- Evd.evar_env evi
-
(* Old style hyps primitive *)
let hyps evars gl =
let evi = content evars gl in