diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-02-05 10:47:44 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-05 10:47:44 +0100 |
commit | 55b2a4e0c24d691b71256c91ed54e245efce340b (patch) | |
tree | 25c65622b9e9e83271d321f399981438b83ff053 /kernel/nativevalues.ml | |
parent | f5cf5e062bdc6264dc3c398ad76559ec188cde47 (diff) | |
parent | 5b8b60508d74bfe5e436ce182889ad8ee6ca3983 (diff) |
Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinition
Diffstat (limited to 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions