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.ml | |
| parent | 28081c1108a84050566d365bd665d05ee508ecce (diff) | |
Remove a useless reversed variant in Vars.
Diffstat (limited to 'kernel/vars.ml')
| -rw-r--r-- | kernel/vars.ml | 3 |
1 files changed, 0 insertions, 3 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 |