diff options
| author | Pierre-Marie Pédrot | 2020-03-28 19:24:53 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-28 19:26:06 +0100 |
| commit | f0ef2d764673670fef52873c441bbbb2f1f7a34d (patch) | |
| tree | 265fd4af6bd0e5190e4a2403a8be4f6b3652be41 /kernel/vars.mli | |
| parent | 28081c1108a84050566d365bd665d05ee508ecce (diff) | |
Remove a useless reversed variant in Vars.
Diffstat (limited to 'kernel/vars.mli')
| -rw-r--r-- | kernel/vars.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/kernel/vars.mli b/kernel/vars.mli index 52a6159f0a..0aac5ed4ce 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -72,9 +72,6 @@ type substl = constr list [c₁], as if usable for [substl]. *) val subst_of_rel_context_instance : Constr.rel_context -> constr list -> substl -(** For compatibility: returns the substitution reversed *) -val adjust_subst_to_rel_context : Constr.rel_context -> 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 |