diff options
| author | Pierre Letouzey | 2017-06-13 12:05:04 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2017-06-14 12:05:03 +0200 |
| commit | c70a21a1c522639138dbcfac53fb2ed96d731d98 (patch) | |
| tree | 4332b2eb79c0065dfbc7daadbc7d3a2d0010fb0c /API/grammar_API.ml | |
| parent | 930662915d75af750db7da1043f9feda321095b3 (diff) | |
[travis] fix CoLoR by inserting some Require Import FunInd
Diffstat (limited to 'API/grammar_API.ml')
0 files changed, 0 insertions, 0 deletions