Illustrat Trac #447

1 files changed, 101 insertions, 0 deletions

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.