diff options
| author | Pierre-Marie Pédrot | 2017-08-26 16:58:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-26 17:36:28 +0200 |
| commit | 7f562a9539522e56004596a751758a08cee798b1 (patch) | |
| tree | fa6d07d099cd6cd13dc5b297c6a56260d38b8bdd /doc | |
| parent | bec2a0ad6eb60d33b5e3ab613d108f456df42a49 (diff) | |
Allowing calls to Ltac2 inside Ltac1.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/ltac2.md | 22 |
1 files changed, 20 insertions, 2 deletions
diff --git a/doc/ltac2.md b/doc/ltac2.md index 5b1776b64f..d1c5c68494 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -698,11 +698,30 @@ errors after expansion. One can call Ltac1 code from Ltac2 by using the `ltac1` quotation. It parses a Ltac1 expression, and semantics of this quotation is the evaluation of the -corresponding code for its side effects. +corresponding code for its side effects. In particular, in cannot return values, +and the quotation has type `unit`. Beware, Ltac1 **cannot** access variables from the Ltac2 scope. One is limited to the use of standalone function calls. +## Ltac2 from Ltac1 + +Same as above by switching Ltac1 by Ltac2 and using the `ltac2` quotation +instead. + +Note that the tactic expression is evaluated eagerly, if one wants to use it as +an argument to a Ltac1 function, she has to resort to the good old +`idtac; ltac2:(foo)` trick. For instance, the code below will fail immediately +and won't print anything. + +``` +Ltac mytac tac := idtac "wow"; tac. + +Goal True. +Proof. +mytac ltac2:(fail). +``` + # Transition from Ltac1 Owing to the use of a bunch of notations, the transition shouldn't be @@ -812,6 +831,5 @@ your duty to catch it and reraise it depending on your use. # TODO - Implement deep pattern-matching. -- Implement compatibility layer with Ltac1 - Craft an expressive set of primitive functions - Implement native compilation to OCaml |