diff options
| author | Maxime Dénès | 2019-04-04 18:17:57 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-10 15:41:43 +0200 |
| commit | 3b980d937b5adfbae472ed8a13748a451fdf3450 (patch) | |
| tree | a3a2fcc4273df543218dbde93a5a5a4934fb0fea /plugins/ltac | |
| parent | 8fe32139aeb965b056c0d1e9c8fab2324dbb7ba6 (diff) | |
Remove calls to global env from indrec
Diffstat (limited to 'plugins/ltac')
0 files changed, 0 insertions, 0 deletions