diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-08 14:36:04 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-08 14:36:04 +0000 |
| commit | 180a27f8d2b7ba2d7913c37ae01c946acb8c813e (patch) | |
| tree | f9b205e4b38bb631b38c0bbfee717fe73d6ae605 /library/kindops.ml | |
| parent | 9d0fde51068c1f1c16142865457a43d2fd5143ee (diff) | |
catch failures of pr_vernac to make -time failsafe
Printing Ltac code is broken. This was not compiling with -time
Ltac pop_succn e := eval lazy beta iota delta [plus] in (1 + 1).
The bug in the pretty printer should be fixed too...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16262 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/kindops.ml')
0 files changed, 0 insertions, 0 deletions