diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-02-02 18:00:07 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-03-24 12:17:35 +0100 |
commit | 68ffb813a0e1c7d62dac4769d0104210c2e5f6e9 (patch) | |
tree | 84056bfd6018a1e1afb757878c3ef376808739ed /parsing/pcoq.mli | |
parent | c6d6e8e5eba5420304fb387430294926cb3fc136 (diff) |
Merging glob_binder and glob_decl.
Diffstat (limited to 'parsing/pcoq.mli')
0 files changed, 0 insertions, 0 deletions