aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
diff options
context:
space:
mode:
authorGravatar Jason Gross <jagro@google.com>2018-07-26 14:40:46 -0400
committerGravatar Jason Gross <jagro@google.com>2018-07-26 14:40:46 -0400
commitca2294ffe37c8ec8f4bf027c9afd3337b10c29d5 (patch)
treecb5f2ce9a522d9d2512b07a3c848a20206b85af7 /_CoqProject
parent201268439584b01c1338ccf3407d929960d74a6d (diff)
Put == in type_scope, so that we don't need to go around opening etype_scope
Diffstat (limited to '_CoqProject')
0 files changed, 0 insertions, 0 deletions