aboutsummaryrefslogtreecommitdiff
path: root/engine/evd.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/evd.ml')
-rw-r--r--engine/evd.ml3
1 files changed, 0 insertions, 3 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index bf519fb7c0..f414d71dc1 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1304,9 +1304,6 @@ let e_eq_constr_univs evdref t u =
let evd, b = eq_constr_univs !evdref t u in
evdref := evd; b
-let eq_constr_univs_test evd t u =
- snd (eq_constr_univs evd t u)
-
(**********************************************************)
(* Accessing metas *)