aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPierre Courtieu2012-06-10 10:40:59 +0000
committerPierre Courtieu2012-06-10 10:40:59 +0000
commit353b3c6a4ecb9b72aa28e02db4374f9d94151e14 (patch)
treefbd20ea788fd593250893e8f330c8003cbc02d00
parent50dea989507462224eaeb1a93d818b87a7e694bb (diff)
Fixing indentation details for coq.
-rw-r--r--coq/coq.el17
1 files changed, 9 insertions, 8 deletions
diff --git a/coq/coq.el b/coq/coq.el
index fb3bdcd4..ea467d37 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -363,12 +363,11 @@ Lemma foo: forall n,
("quantif exists" exp "," exp)
("forall" exp "," exp)
("(" exps ")") ("{|" exps "|}") ("{" exps "}") ("[" expssss "]")
- (exp "<->" exp) (exp "/\\" exp) (exp "\\/" exp)
- (exp "==" exp) (exp "^" exp) (exp "+" exp)
- (exp "-" exp) (exp "*" exp) ;(exp "/" exp)
- (exp "=" exp) (exp "<>" exp) (exp "<=" exp) (exp "<" exp)
- (exp ">=" exp) (exp ">" exp) (exp "=?" exp) (exp "<=?" exp)
- (exp "<?" exp) (exp "->" exp)
+ (exp "->" exp) (exp "<->" exp) (exp "/\\" exp) (exp "\\/" exp)
+ (exp "==" exp) (exp "=" exp) (exp "<>" exp) (exp "<=" exp)
+ (exp "<" exp) (exp ">=" exp) (exp ">" exp)
+ (exp "=?" exp) (exp "<=?" exp) (exp "<?" exp)
+ (exp "^" exp) (exp "+" exp) (exp "-" exp) (exp "*" exp)
(exp ":" exp))
;; Having "return" here rather than as a separate rule in `exp' causes
;; it to be indented at a different level than "with".
@@ -414,13 +413,15 @@ Lemma foo: forall n,
(cmds "." cmds)))
;; Resolve the "trailing expression ambiguity" as in "else x -> b".
;; each line orders tokens by increasing proprity
- '((left ",") (assoc ":") (assoc "->") (left "<->")
+ '((left ",") (assoc ":")
+ (assoc "\\/") (assoc "/\\")
+ (assoc "->") (left "<->")
(assoc "<?") (assoc "<=?") (assoc "=?") (assoc ">") (assoc ">=")
(assoc "<") (assoc "<=") (left "<>") (left "=") (left "==")
(nonassoc "else") (nonassoc "in") (assoc "in tactic")
(assoc ":= record") (assoc "; record") (left "=>")
(left "^")
- (assoc "-")(assoc "+") (assoc "\\/") (assoc "*") (assoc "/\\"))
+ (assoc "-")(assoc "+") (assoc "*") )
'((left ",")(assoc ";")(right "as")(left "|")(left "=>"))
'((left "- bullet") (left "+ bullet") (left "* bullet"))
'((assoc ".")))))