diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-06-23 18:48:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-06-23 18:57:10 +0200 |
| commit | 47860acaffe6017c3b5165d6442f9fbf5c524495 (patch) | |
| tree | 573f7dc2d364209733ba5a1b1f5bac97f0390e22 /tactics/tacintern.ml | |
| parent | 5f7adad4af7d526aed3a97f8b24b2d9811f9fea7 (diff) | |
Less closures makes the GC happy.
Diffstat (limited to 'tactics/tacintern.ml')
0 files changed, 0 insertions, 0 deletions