diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-17 09:06:09 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-03-17 09:06:09 +0100 |
| commit | ac3ee8cba2d27f2be38ba706e49aeee08086d936 (patch) | |
| tree | 67c2633ac657abd1b5bc2a26b27b7cb7a9aad868 /plugins/ltac/tacinterp.ml | |
| parent | f2bbdd31a6aa62d8a000f5a91f666e68e7241964 (diff) | |
| parent | 105f346cc707b3433379514cd5ddcd3389912083 (diff) | |
Merge PR#437: Improve unification debug trace.
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
0 files changed, 0 insertions, 0 deletions