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/indtypes.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'kernel/indtypes.ml')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index e4bf055c95..383bdc2ef3 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -354,6 +354,11 @@ if nmr = 0 then 0 else
           | _ -> k)
   in find 0 (n-1) (lpar,List.rev hyps)
 
+let lambda_implicit_lift n a =
+  let implicit_sort = mkType (make_univ (make_dirpath [id_of_string "implicit"], 0)) in
+  let lambda_implicit a = mkLambda (Anonymous, implicit_sort, a) in
+  iterate lambda_implicit n (lift n a)
+
 (* This removes global parameters of the inductive types in lc (for
    nested inductive types only ) *)
 let abstract_mind_lc env ntyps npars lc =
-- 
cgit v1.2.3