From 6899d3aa567436784a08af4e179c2ef1fa504a02 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 21 Nov 2015 00:17:21 +0100
Subject: Moving extended_rel_vect/extended_rel_list to the kernel.

It will later be used to fix a bug and improve some code.

Interestingly, there were a redundant semantic equivalent to
extended_rel_list in the kernel called local_rels, and another private
copy of extended_rel_list in exactly the same file.
---
 engine/termops.ml  | 13 -------------
 engine/termops.mli |  4 ----
 2 files changed, 17 deletions(-)

(limited to 'engine')

diff --git a/engine/termops.ml b/engine/termops.ml
index 63baec129e..db0f1e4db5 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -158,19 +158,6 @@ 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)
-
-
-
 let push_rel_assum (x,t) env = push_rel (x,None,t) env
 
 let push_rels_assum assums =
diff --git a/engine/termops.mli b/engine/termops.mli
index 94c485a261..87f74f7435 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -37,13 +37,9 @@ val lookup_rel_id : Id.t -> rel_context -> int * constr option * types
 
 (** Functions that build argument lists matching a block of binders or a context.
     [rel_vect n m] builds [|Rel (n+m);...;Rel(n+1)|]
-    [extended_rel_vect n ctx] extends the [ctx] context of length [m]
-    with [n] elements.
 *)
 val rel_vect : int -> int -> constr array
 val rel_list : int -> int -> constr list
-val extended_rel_list : int -> rel_context -> constr list
-val extended_rel_vect : int -> rel_context -> constr array
 
 (** iterators/destructors on terms *)
 val mkProd_or_LetIn : rel_declaration -> types -> types
-- 
cgit v1.2.3