aboutsummaryrefslogtreecommitdiff
path: root/kernel/retroknowledge.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2021-03-18 22:21:19 +0100
committerPierre-Marie Pédrot2021-03-18 22:23:44 +0100
commitb809bf80bed06303f3d5aa2297787782a030f037 (patch)
treed36666d59244fec29e968d3b0e2cd90efe94ea0a /kernel/retroknowledge.ml
parenteeef63b0b09cf90f7a3022ce6f0d7e50a908484c (diff)
Implement ! goal selector for Ltac2.
Fixes #13960: Ltac2 Eval does not work with Set Default Goal Selector "!".
Diffstat (limited to 'kernel/retroknowledge.ml')
0 files changed, 0 insertions, 0 deletions