summaryrefslogtreecommitdiff
path: root/interp/coqlib.mli
diff options
context:
space:
mode:
Diffstat (limited to 'interp/coqlib.mli')
-rw-r--r--interp/coqlib.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 986a4385..41204a71 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -160,7 +160,6 @@ val build_coq_sumbool : constr delayed
(** Connectives
The False proposition *)
val build_coq_False : constr delayed
-val build_coq_proof_admitted : constr delayed
(** The True proposition and its unique proof *)
val build_coq_True : constr delayed