From 4ff5aea548076b6f0fd9ebca3cae0959681b35bb Mon Sep 17 00:00:00 2001
From: glondu
Date: Wed, 3 Nov 2010 09:54:09 +0000
Subject: Remove suspiciously named "implicit" stuff from Term

The lambda_implicit series of functions are used only in Indtypes, so
we move them there. In the checker, they are already there...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13615 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term.mli | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'kernel/term.mli')

diff --git a/kernel/term.mli b/kernel/term.mli
index 875ac89896..848befbeca 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -368,10 +368,6 @@ val mkNamedLambda_or_LetIn : named_declaration -> constr -> constr
 
 (** {6 Other term constructors. } *)
 
-val abs_implicit : constr -> constr
-val lambda_implicit : constr -> constr
-val lambda_implicit_lift : int -> constr -> constr
-
 (** [applist (f,args)] and its variants work as [mkApp] *)
 
 val applist : constr * constr list -> constr
-- 
cgit v1.2.3