diff options
| author | Pierre Courtieu | 2012-06-10 10:40:59 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2012-06-10 10:40:59 +0000 |
| commit | 353b3c6a4ecb9b72aa28e02db4374f9d94151e14 (patch) | |
| tree | fbd20ea788fd593250893e8f330c8003cbc02d00 | |
| parent | 50dea989507462224eaeb1a93d818b87a7e694bb (diff) | |
Fixing indentation details for coq.
| -rw-r--r-- | coq/coq.el | 17 |
1 files changed, 9 insertions, 8 deletions
@@ -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 "."))))) |
