aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/auto_ind_decl.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-02 09:23:11 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-02 09:23:11 +0200
commit249b19897671b95ce0a3b8aba6b24005a315bb8c (patch)
tree36391833049dbab750b8e5de73f8d53091edd3f6 /vernac/auto_ind_decl.ml
parent991b78fd9627ee76f1a1a39b8460bf361c6af53d (diff)
parent540588e7c1e7edc3ced91f2c5b544025da0681f5 (diff)
Merge PR#595: Avoiding registering files from _build_ci for computing dependencies
Diffstat (limited to 'vernac/auto_ind_decl.ml')
0 files changed, 0 insertions, 0 deletions