From f35cee3e3b2cf29822d887a5749800bd311aa971 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 18 May 2000 08:16:56 +0000
Subject: Ajout lift_context

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@443 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/generic.ml  | 3 +++
 kernel/generic.mli | 6 ++++++
 2 files changed, 9 insertions(+)

(limited to 'kernel')

diff --git a/kernel/generic.ml b/kernel/generic.ml
index 329103fa14..2a8af630da 100644
--- a/kernel/generic.ml
+++ b/kernel/generic.ml
@@ -148,6 +148,9 @@ let liftn k n =
 let lift k = liftn k 1
 let lift1 c = exliftn (ELSHFT(ELID,1)) c
 
+let lift_context n l = 
+  let k = List.length l in 
+  list_map_i (fun i (name,c) -> (name,liftn n (k-i) c)) 0 l
 
 (* explicit substitutions of type 'a *)
 type 'a subs =
diff --git a/kernel/generic.mli b/kernel/generic.mli
index 61686e9702..6825c3978b 100644
--- a/kernel/generic.mli
+++ b/kernel/generic.mli
@@ -52,6 +52,12 @@ val liftn : int -> int -> 'a term -> 'a term
 val lift : int -> 'a term -> 'a term
 val pop : 'a term -> 'a term
 
+(* [lift_context n ctxt] lifts terms in [ctxt] by [n] preserving
+   (i.e. not lifting) the internal references between terms of [ctxt];
+   more recent terms come first in [ctxt] *)
+
+val lift_context : int -> (name * 'a term) list -> (name * 'a term) list
+
 (*s Explicit substitutions of type ['a]. [ESID] = identity. 
   [CONS(t,S)] = $S.t$ i.e. parallel substitution. [SHIFT(n,S)] = 
   $(\uparrow n~o~S)$ i.e. terms in S are relocated with n vars. 
-- 
cgit v1.2.3