From 0dc79e09b2b7c369b35191191aa257451a536540 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 11 Mar 2018 01:14:28 +0100 Subject: [api] Remove deprecated objects in engine / interp / library --- library/globnames.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'library/globnames.ml') diff --git a/library/globnames.ml b/library/globnames.ml index 6b78d12ba..6383a1f8f 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -87,8 +87,6 @@ let printable_constr_of_global = function | ConstructRef sp -> mkConstruct sp | IndRef sp -> mkInd sp -let reference_of_constr = global_of_constr - let global_eq_gen eq_cst eq_ind eq_cons x y = x == y || match x, y with -- cgit v1.2.3