aboutsummaryrefslogtreecommitdiff
path: root/dev/include
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-12-06 10:01:41 +0100
committerGitHub2018-12-06 10:01:41 +0100
commitf503e20667008eabb48aa1676ce56f4958c7087e (patch)
tree94333b1e21124e4394dbd722276c37a62662f7a7 /dev/include
parent550472c67198353120cdc02b42683024b5b39765 (diff)
parente2fe373a1947206746dd43afe6c9815c69453def (diff)
Merge pull request coq/ltac2#90 from ejgallego/tests
[build] Test tests in Travis, use coqc for tests.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions