From ba9806a242c7ece41a93181d1fb91279c89794ed Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 2 May 2017 16:10:19 +0200 Subject: Remove dead code in native compiler. --- kernel/nativecode.ml | 12 ------------ 1 file changed, 12 deletions(-) (limited to 'kernel/nativecode.ml') diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index ba80ff590..5130aa9a4 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -42,8 +42,6 @@ module LNset = Set.Make(LNord) let lname_ctr = ref (-1) -let reset_lname = lname_ctr := -1 - let fresh_lname n = incr lname_ctr; { lname = n; luid = !lname_ctr } @@ -112,40 +110,30 @@ let gname_hash gn = match gn with let case_ctr = ref (-1) -let reset_gcase () = case_ctr := -1 - let fresh_gcase l = incr case_ctr; Gcase (l,!case_ctr) let pred_ctr = ref (-1) -let reset_gpred () = pred_ctr := -1 - let fresh_gpred l = incr pred_ctr; Gpred (l,!pred_ctr) let fixtype_ctr = ref (-1) -let reset_gfixtype () = fixtype_ctr := -1 - let fresh_gfixtype l = incr fixtype_ctr; Gfixtype (l,!fixtype_ctr) let norm_ctr = ref (-1) -let reset_norm () = norm_ctr := -1 - let fresh_gnorm l = incr norm_ctr; Gnorm (l,!norm_ctr) let normtbl_ctr = ref (-1) -let reset_normtbl () = normtbl_ctr := -1 - let fresh_gnormtbl l = incr normtbl_ctr; Gnormtbl (l,!normtbl_ctr) -- cgit v1.2.3