diff options
-rw-r--r-- | coq/coq.el | 5 | ||||
-rw-r--r-- | coq/ex/indent.v | 9 |
2 files changed, 9 insertions, 5 deletions
@@ -366,6 +366,8 @@ Lemma foo: forall n, ("{|" exps "|}") ("{" exps "}") ("[" expssss "]") + (exp "<->" exp) + (exp "=" exp) (exp "->" exp) (exp ":" exp)) ;; Having "return" here rather than as a separate rule in `exp' causes @@ -409,7 +411,8 @@ Lemma foo: forall n, ;; stops right before the "." rather than right after. (cmds "." cmds))) ;; Resolve the "trailing expression ambiguity" as in "else x -> b". - '((assoc ",") (nonassoc "as") (assoc ":") (assoc "->") (nonassoc "else") + '((assoc ",") (nonassoc "as") (assoc ":") (assoc "->") + (assoc "=") (assoc "<->") (nonassoc "else") (nonassoc "in") (assoc "in tactic") (left "=>")) '((assoc ",")(assoc ";")(assoc "|")(left "=>")) '((left "- bullet") (left "+ bullet") (left "* bullet")) diff --git a/coq/ex/indent.v b/coq/ex/indent.v index 28a56515..a6fda706 100644 --- a/coq/ex/indent.v +++ b/coq/ex/indent.v @@ -174,10 +174,11 @@ Module X. Lemma l2 : forall r:rec, - exists r':rec,r'.(fld1) - = r.(fld2) - /\ r'.(fld2) - = r.(fld1). + exists r':rec, + ressai.(fld1) + = r.(fld2) + /\ r'.(fld2) + = r.(fld1). Proof. intros r. {{ |