diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-12 11:27:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-12 11:27:07 +0200 |
| commit | 52c583660d3d7aa5eddf209632a46276ff9e4236 (patch) | |
| tree | 7ced217f73f62babc4c0e3c8c44e14a17d29b9ca /test-suite/success | |
| parent | 32b424902383a99436439a3c8ee24a528d1077a9 (diff) | |
| parent | acf5e4b0a7bae99263f76e7330fd85c56c4eda68 (diff) | |
Merge PR #7096: coqide: avoid marking sentences that are not in the document anymore
Diffstat (limited to 'test-suite/success')
0 files changed, 0 insertions, 0 deletions