From 80bbdf335be5657f5ab33b4aa02e21420d341de2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 17:11:03 +0100 Subject: Remove some unused functions. Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot. --- kernel/declareops.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'kernel/declareops.ml') diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 73cfd0122..803df7827 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -391,5 +391,3 @@ and hcons_module_body mb = mod_delta = delta'; mod_retroknowledge = retroknowledge'; } - -and hcons_module_type_body mtb = hcons_module_body mtb -- cgit v1.2.3