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.ml | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'kernel/term.ml')

diff --git a/kernel/term.ml b/kernel/term.ml
index 5c1fcabf8d..eaa326613c 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -973,18 +973,10 @@ let mkFix = mkFix
 *)
 let mkCoFix = mkCoFix
 
-(* Construct an implicit *)
-let implicit_sort = Type (make_univ(make_dirpath[id_of_string"implicit"],0))
-let mkImplicit = mkSort implicit_sort
-
 (***************************)
 (* Other term constructors *)
 (***************************)
 
-let abs_implicit c = mkLambda (Anonymous, mkImplicit, c)
-let lambda_implicit a = mkLambda (Name(id_of_string"y"), mkImplicit, a)
-let lambda_implicit_lift n a = iterate lambda_implicit n (lift n a)
-
 (* prodn n [xn:Tn;..;x1:T1;Gamma] b = (x1:T1)..(xn:Tn)b *)
 let prodn n env b =
   let rec prodrec = function
-- 
cgit v1.2.3