aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPierre Courtieu2020-01-13 15:35:51 +0100
committerPierre Courtieu2020-01-13 15:35:51 +0100
commitbee3f802ada921fb8988edb96a8b41429f7c622c (patch)
tree52c9c3a5b79313296e06276730f1b4db64baf04e
parentcf904b955056f16e46d1541b3ffb1ca1533c936d (diff)
Fixing /\ and \/ priority for indentation purpose.
-rw-r--r--coq/coq-smie.el2
1 files changed, 1 insertions, 1 deletions
diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index 6a92113d..6155d0fc 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -953,7 +953,7 @@ Typical values are 2 or 4."
(assoc "|-") (assoc ":" ":<") (assoc ",")
(assoc "else")
(assoc "->") (assoc "<->")
- (assoc "&") (assoc "/\\") (assoc "\\/")
+ (assoc "\\/") (assoc "&") (assoc "/\\")
(assoc "==") (assoc "=") (assoc "<" ">" "<=" ">=" "<>")
(assoc "=?") (assoc "<=?") (assoc "<?") (assoc "^")
(assoc "||") ;; FIXME: detecting "+ tactic" and "|| tactic" seems impossible