[sledge] Fix Context.apply_subst to preserve rest of representation

Summary:
Context.apply_subst erroneously resets everything in the
representation of a context except the solution substitution when
applying a substitution.

Reviewed By: jvillard

Differential Revision: D25756548

fbshipit-source-id: 949a34ced
master
Josh Berdine 4 years ago committed by Facebook GitHub Bot
parent e0312f1274
commit a7b547ccdf

@ -683,7 +683,8 @@ let apply_subst wrt s r =
;
( if Subst.is_empty s then r
else
Trm.Map.fold (classes r) empty ~f:(fun ~key:rep ~data:cls r ->
Trm.Map.fold (classes r) {r with rep= Subst.empty}
~f:(fun ~key:rep ~data:cls r ->
let rep' = Subst.subst_ s rep in
List.fold cls r ~f:(fun trm r ->
let trm' = Subst.subst_ s trm in

Loading…
Cancel
Save