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.
---
 interp/constrextern.ml | 9 ---------
 1 file changed, 9 deletions(-)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index ed85c38de0..5c9e80df3d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -462,15 +462,6 @@ let is_needed_for_correct_partial_application tail imp =
 
 exception Expl
 
-let params_implicit n impl = 
-  let rec aux n impl =
-    if n == 0 then true
-    else match impl with
-    | [] -> false
-    | imp :: impl when is_status_implicit imp -> aux (pred n) impl
-    | _ -> false
-  in aux n impl
-
 (* Implicit args indexes are in ascending order *)
 (* inctx is useful only if there is a last argument to be deduced from ctxt *)
 let explicitize loc inctx impl (cf,f) args =
-- 
cgit v1.2.3