diff options
| author | Pierre-Marie Pédrot | 2020-04-23 16:46:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-23 16:46:25 +0200 |
| commit | cddd0149b686b247116681a17b5c7bf42d513115 (patch) | |
| tree | f8696c9ad900efd1b54bd9ca84daddf12fdb580f /lib/objFile.ml | |
| parent | 48f73e492465f3c46438583c069bc0ba745ef56f (diff) | |
| parent | 8de0fcaa08c82ece8874606e8fa1954d860bd88e (diff) | |
Merge PR #12130: [declare] [tactics] Move declare to `vernac`
Reviewed-by: ppedrot
Diffstat (limited to 'lib/objFile.ml')
0 files changed, 0 insertions, 0 deletions