diff options
| author | Hugo Herbelin | 2014-12-04 09:53:41 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-04 11:42:58 +0100 |
| commit | 84694dcd9b720d4ed7eb838ad7c5a083e7eb86fe (patch) | |
| tree | e2213b513b56a172f0e0616d601244955d13a2cb /pretyping | |
| parent | 21a1c8abdd5807427849c34875c294cb6ad7d899 (diff) | |
coqdep: granting #2506 (./dir is the same as dir)
Diffstat (limited to 'pretyping')
0 files changed, 0 insertions, 0 deletions