diff options
| author | Gaëtan Gilbert | 2020-03-30 13:04:47 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-03-30 13:04:47 +0200 |
| commit | e21aae1b32adba4e8673783f327826d279e05ced (patch) | |
| tree | d20413576f188f661914d38279f8b7d592186b95 /kernel | |
| parent | 7ff44dd02d935cb078487629b342b7106cc72955 (diff) | |
| parent | f0ef2d764673670fef52873c441bbbb2f1f7a34d (diff) | |
Merge PR #11951: Remove a useless reversed variant in Vars.
Reviewed-by: SkySkimmer
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/vars.ml | 3 | ||||
| -rw-r--r-- | kernel/vars.mli | 3 |
2 files changed, 0 insertions, 6 deletions
diff --git a/kernel/vars.ml b/kernel/vars.ml index 4c66f1574f..a4465c293b 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -169,9 +169,6 @@ let subst_of_rel_context_instance sign l = | _ -> CErrors.anomaly (Pp.str "Instance and signature do not match.") in aux [] (List.rev sign) l -let adjust_subst_to_rel_context sign l = - List.rev (subst_of_rel_context_instance sign l) - let adjust_rel_to_rel_context sign n = let rec aux sign = let open RelDecl in 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 |