diff options
| author | Pierre-Marie Pédrot | 2019-09-25 14:32:39 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-09-25 14:32:39 +0200 |
| commit | 227fcc4dff6fbb68ad6b91387b2f36705329a57e (patch) | |
| tree | 054ab24af9d4649103763355745ff60c6204fe14 /library/lib.mli | |
| parent | 4e022849b7119e3a51b46fa73132b3e3cc7927ab (diff) | |
| parent | f92b5e4a91e8edb7ccac2ebe64d68c8d89e2e0db (diff) | |
Merge PR #10784: Fix #10783: use binder_annot in Ltac2.Constr.Unsafe.kind
Reviewed-by: ppedrot
Diffstat (limited to 'library/lib.mli')
0 files changed, 0 insertions, 0 deletions