Commit 84910af8 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix typo in comment.

parent 51d94abb
...@@ -766,7 +766,7 @@ Tactic Notation "iIntoEmpValid" open_constr(t) := ...@@ -766,7 +766,7 @@ Tactic Notation "iIntoEmpValid" open_constr(t) :=
[lazy_tc] denotes whether type class inference on the premises of [lem] should [lazy_tc] denotes whether type class inference on the premises of [lem] should
be performed before (if false) or after (if true) [tac H] is called. be performed before (if false) or after (if true) [tac H] is called.
The tactic [iApply] uses laxy type class inference, so that evars can first be The tactic [iApply] uses lazy type class inference, so that evars can first be
instantiated by matching with the goal, whereas [iDestruct] does not, because instantiated by matching with the goal, whereas [iDestruct] does not, because
eliminations may not be performed when type classes have not been resolved. eliminations may not be performed when type classes have not been resolved.
*) *)
......
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