diff options
| author | Pierre-Marie Pédrot | 2019-06-08 15:20:41 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-08 15:20:41 +0200 |
| commit | 65f75de6929530252a3235af54a0da56980fa02d (patch) | |
| tree | b61d06dc1a3b78f6390fb929bb0fa73eb73e2a2d /engine | |
| parent | 0d97f184408ffd50d11608f0e73ac3edaf1193ca (diff) | |
| parent | fe49db8833803f87e2f750b698f28868d276bfe6 (diff) | |
Merge PR #10289: [Ltac2] “constr” arguments to tactic notations may have interpretation scopes
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
Ack-by: vbgl
Diffstat (limited to 'engine')
0 files changed, 0 insertions, 0 deletions