diff options
| author | Maxime Dénès | 2017-11-13 11:26:36 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-13 11:26:36 +0100 |
| commit | c232059eecefa8763ce1e381990d6d7034080d3e (patch) | |
| tree | 75acd1f013fe96a2a971b3a4d479fde05516c9b9 /lib/cErrors.ml | |
| parent | 515855523b478433db8e9a0db21ca2e762c14dac (diff) | |
| parent | 4e23d4b7ba4910e7c41d2cbc4c3bff12ba153558 (diff) | |
Merge PR #6103: Hack to restore printing of glob_constr in debugger.
Diffstat (limited to 'lib/cErrors.ml')
0 files changed, 0 insertions, 0 deletions