diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-05 15:35:41 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-05 15:35:41 -0400 |
| commit | c4a0d1fdde22dbd2faaa1753e973ee9602076ee8 (patch) | |
| tree | 1234bab3d75fe11e7f165f526a4a29be715424c6 | |
| parent | b9770718be4f65de7b0cdfcd1c08000e5eac8ca4 (diff) | |
Allow loop notation to print
With help from Hugo at https://coq.inria.fr/bugs/show_bug.cgi?id=5581#c1
cc @andres-erbsen
| -rw-r--r-- | src/Util/Loop.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Util/Loop.v b/src/Util/Loop.v index 0922440a3..7b639fe4d 100644 --- a/src/Util/Loop.v +++ b/src/Util/Loop.v @@ -95,9 +95,9 @@ End with_state. (* N.B., Coq doesn't yet print this *) Notation "'loop' _{ fuel } ( state1 .. staten = initial ) 'via' ( continue , break ) {{ body }} ; rest" := (@loop_cps _ fuel initial - (fun state1 => .. (fun staten => (fun _ continue break => body)) .. ) + (fun state1 => .. (fun staten => id (fun T continue break => body)) .. ) _ (fun state1 => .. (fun staten => rest) .. )) - (at level 200, state1 binder, staten binder, rest at level 10, only parsing, + (at level 200, state1 binder, staten binder, rest at level 10, format "'[v ' 'loop' _{ fuel } ( state1 .. staten = initial ) 'via' ( continue , break ) {{ '//' body ']' '//' }} ; '//' rest"). Check loop _{ 10 } (x = 0) via (continue, break) {{ continue (x + 1) }} ; x. |