From 82996a5df1bf7a2c09efbf42d49e9a1420bc8abc Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Mon, 27 Aug 2012 12:30:16 +0000 Subject: Illustrat Trac #447 --- etc/coq/bug-447.v | 101 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 101 insertions(+) create mode 100644 etc/coq/bug-447.v (limited to 'etc/coq/bug-447.v') diff --git a/etc/coq/bug-447.v b/etc/coq/bug-447.v new file mode 100644 index 00000000..cc7ccc69 --- /dev/null +++ b/etc/coq/bug-447.v @@ -0,0 +1,101 @@ +Ltac bar k := k tt. + +(* The next tactic definition seems to get stuck when processing in PG. + It works fine typed into coqtop and also works if a couple of the + match lines are removed. + + It does seem to be something to do with the line length, as if + the lines are commented out the same problem happens. + + See http://proofgeneral.inf.ed.ac.uk/trac/ticket/447 +*) +Ltac foo x := + bar ltac:(fun a => + bar ltac:(fun b => + bar ltac:(fun c => + bar ltac:(fun d => + bar ltac:(fun e => + bar ltac:(fun f => + bar ltac:(fun g => + bar ltac:(fun h => + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + let x := match tt with | tt => constr:(1) end in + idtac)))))))). + +Ltac wim x := foo x. -- cgit v1.2.3