diff options
| author | Clément Pit-Claudel | 2019-02-06 11:42:13 -0500 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-02-06 11:42:13 -0500 |
| commit | 7886c6d8e0663ba346fff52837012c7fc952ecc1 (patch) | |
| tree | 6328dcd9a7abf1ebb79aab558461edd0c1acdd77 /dev | |
| parent | 177a438806f811901ad0aeab4ed69014e9d2af26 (diff) | |
| parent | 4031789bd30dabdfad941f6ca3a77862057fae58 (diff) | |
Merge PR #9124: Document the possibility of declaring a Ltac name_goal.
Reviewed-by: cpitclaudel
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions