From ade2363e357db3ac3f258e645fe6bba988e7e7dd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 19 Nov 2015 22:49:25 +0100
Subject: About building of substitutions from instances.

Redefining adjust_subst_to_rel_context from instantiate_context who
was hidden in inductiveops.ml, renamed the latter into
subst_of_rel_context_instance and moving them to Vars. The new name
highlights that the input is an instance (as for applist) and the
output a substitution (as for substl). This is a clearer unified
interface, centralizing the difficult de-Bruijn job in one place. It
saves a couple of List.rev.
---
 engine/termops.ml  | 10 ----------
 engine/termops.mli |  2 +-
 2 files changed, 1 insertion(+), 11 deletions(-)

(limited to 'engine')

diff --git a/engine/termops.ml b/engine/termops.ml
index 5716a19dd1..63baec129e 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -953,16 +953,6 @@ let smash_rel_context sign =
       aux (List.rev (substl_rel_context [b] (List.rev acc))) l
   in List.rev (aux [] sign)
 
-let adjust_subst_to_rel_context sign l =
-  let rec aux subst sign l =
-    match sign, l with
-    | (_,None,_)::sign', a::args' -> aux (a::subst) sign' args'
-    | (_,Some c,_)::sign', args' ->
-	aux (substl subst c :: subst) sign' args'
-    | [], [] -> List.rev subst
-    | _ -> anomaly (Pp.str "Instance and signature do not match")
-  in aux [] (List.rev sign) l
-
 let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init
 
 let rec mem_named_context id = function
diff --git a/engine/termops.mli b/engine/termops.mli
index 5d812131ed..94c485a261 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -219,7 +219,7 @@ val assums_of_rel_context : rel_context -> (Name.t * constr) list
 val lift_rel_context : int -> rel_context -> rel_context
 val substl_rel_context : constr list -> rel_context -> rel_context
 val smash_rel_context : rel_context -> rel_context (** expand lets in context *)
-val adjust_subst_to_rel_context : rel_context -> constr list -> constr list
+
 val map_rel_context_in_env :
   (env -> constr -> constr) -> env -> rel_context -> rel_context
 val map_rel_context_with_binders :
-- 
cgit v1.2.3