Commit e0780ad4 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen

Add a comment on the simplifier tactic

parent ff904e6e
Pipeline #12219 failed with stage
in 22 seconds
......@@ -742,6 +742,10 @@ Local Ltac simpl_exp_invariant exp :=
rewrite num_outgoing_acts_app
end.
(* This tactic performs various simplifications on the goal involving
expressions establishing the invariant. For instance, it tries to rewrite
num_cacts_in_state (add_tx tx env) -> num_cacts_in_state env using some
common tactics. *)
Local Ltac simpl_goal_invariant :=
repeat
match goal with
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment