From c4a0d1fdde22dbd2faaa1753e973ee9602076ee8 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 5 Jun 2017 15:35:41 -0400 Subject: Allow loop notation to print With help from Hugo at https://coq.inria.fr/bugs/show_bug.cgi?id=5581#c1 cc @andres-erbsen --- src/Util/Loop.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Util') 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. -- cgit v1.2.3