aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
authorCyril Cohen2019-04-29 17:26:22 +0200
committerCyril Cohen2019-04-29 17:26:22 +0200
commit05c5c3ab8e52ebe43179975b42142f2646b0479e (patch)
treedf53ce204a27483dd25bcaad8c70a78aa5398312 /ide
parentf08880552350310df8a60ec37d6ada9d0ef1b40f (diff)
parent92e2bb2bebc99b6a72ea0babad9a1c374129a0c0 (diff)
Merge PR #9651: [ssr] Add tactics under and over
Reviewed-by: CohenCyril Ack-by: Zimmi48 Ack-by: erikmd Ack-by: gares Ack-by: jfehrle
Diffstat (limited to 'ide')
-rw-r--r--ide/coq-ssreflect.lang2
1 files changed, 2 insertions, 0 deletions
diff --git a/ide/coq-ssreflect.lang b/ide/coq-ssreflect.lang
index bd9cb4bfa2..fc7bc64a68 100644
--- a/ide/coq-ssreflect.lang
+++ b/ide/coq-ssreflect.lang
@@ -73,11 +73,13 @@
<keyword>suffices</keyword>
<keyword>suff</keyword>
<keyword>transitivity</keyword>
+ <keyword>under</keyword>
<keyword>without loss</keyword>
<keyword>wlog</keyword>
</context>
<context id="ssr-endtac" style-ref="endtactic">
<keyword>by</keyword>
+ <keyword>over</keyword>
<keyword>exact</keyword>
<keyword>reflexivity</keyword>
</context>