pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

explain why recursive [inster] can fail

Browse source
This commit is contained in:
Samuel Gruetter 2020-03-01 22:30:35 -05:00
parent 096b69a3e9
commit 74e2399343
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
IntroToProofScripting.v
View file

@ -518,7 +518,8 @@ Ltac inster n :=
end end
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! *) * [match goal] cause us to try the next instantiation! *)
Section test_inster. Section test_inster.