aboutsummaryrefslogtreecommitdiff
path: root/kernel/evd.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/evd.mli')
-rw-r--r--kernel/evd.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/kernel/evd.mli b/kernel/evd.mli
index 6c0e6a716e..f6192c7e50 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -22,8 +22,6 @@ open Sign
type evar = int
-val new_evar : unit -> evar
-
type evar_body =
| Evar_empty
| Evar_defined of constr