From 5c1768a4dcf39ffd7d58ea9448a842376e86ccf9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 5 Mar 2001 08:20:05 +0000
Subject: Re-Déplacement extended_rel_list

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

(limited to 'kernel/term.ml')

diff --git a/kernel/term.ml b/kernel/term.ml
index 533f013e4d..c979577c9c 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1225,6 +1225,17 @@ let rel_list n m =
   in 
   reln [] 1
 
+(* Same as [rel_list] but takes a context as argument and skips let-ins *)
+let extended_rel_list n hyps =
+  let rec reln l p = function
+    | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps
+    | (_,Some _,_) :: hyps -> reln l (p+1) hyps
+    | [] -> l
+  in 
+  reln [] 1 hyps
+
+let extended_rel_vect n hyps = Array.of_list (extended_rel_list n hyps)
+
 (*********************************)
 (* Other term destructors        *)
 (*********************************)
-- 
cgit v1.2.3