aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/libnames.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/libnames.ml')
-rw-r--r--library/libnames.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/library/libnames.ml b/library/libnames.ml
index 4d25c42f9..dcdd5ac41 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -49,10 +49,8 @@ let constr_of_global = function
| ConstructRef sp -> mkConstruct sp
| IndRef sp -> mkInd sp
-(*
let constr_of_reference = constr_of_global
let reference_of_constr = global_of_constr
-*)
module RefOrdered =
struct