diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-07 22:27:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-07 23:03:54 +0200 |
| commit | 87f9a317b020554abef358aec614dad1fdc0bd98 (patch) | |
| tree | 9eb50003907da13dc1c6078e80dc0d6706189136 /test-suite/bugs/closed/4684.v | |
| parent | 9169e5ffbf5d55d09dfc91bcf6c73f71c451387c (diff) | |
Fix bug #4777: Printing time is impacted by large terms that don't print.
We delay the externalization of application arguments in Constrextern,
so that they only get computed when they are actually explicitly displayed.
Diffstat (limited to 'test-suite/bugs/closed/4684.v')
0 files changed, 0 insertions, 0 deletions