Merge pull request #36 from samuelgruetter/ltac_lecture_comment

explain why recursive [inster] can fail
This commit is contained in:
Adam Chlipala 2020-03-02 11:45:36 -05:00 committed by GitHub
commit 19d915fb37
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -518,7 +518,8 @@ Ltac inster n :=
end
end.
(* Important: when one recursive call fails, the backtracking semantics of
(* Important: when one recursive call fails (happens when [n] reaches zero and
* [intuition] leaves some open goals), the backtracking semantics of
* [match goal] cause us to try the next instantiation! *)
Section test_inster.