aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/vars.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/vars.mli')
-rw-r--r--kernel/vars.mli4
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/vars.mli b/kernel/vars.mli
index 574d50ecc..adeac422e 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -73,6 +73,10 @@ val subst_of_rel_context_instance : Context.Rel.t -> constr list -> substl
(** For compatibility: returns the substitution reversed *)
val adjust_subst_to_rel_context : Context.Rel.t -> constr list -> constr list
+(** Take an index in an instance of a context and returns its index wrt to
+ the full context (e.g. 2 in [x:A;y:=b;z:C] is 3, i.e. a reference to z) *)
+val adjust_rel_to_rel_context : ('a, 'b) Context.Rel.pt -> int -> int
+
(** [substnl [a₁;...;an] k c] substitutes in parallel [a₁],...,[an]
for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates
accordingly indexes in [an],...,[a1] and [c]. In terms of typing, if