aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/coqlib.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/coqlib.ml')
-rw-r--r--library/coqlib.ml4
1 files changed, 0 insertions, 4 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml
index 8787738af..141fff033 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -377,7 +377,3 @@ let coq_sumbool_ref = lazy (init_reference ["Specif"] "sumbool")
let coq_sig_ref = lazy (init_reference ["Specif"] "sig")
let coq_or_ref = lazy (init_reference ["Logic"] "or")
let coq_iff_ref = lazy (init_reference ["Logic"] "iff")
-
-(* Deprecated *)
-let gen_reference = coq_reference
-