aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/ex
diff options
context:
space:
mode:
authorGravatar Stefan Monnier <monnier@iro.umontreal.ca>2014-06-06 17:23:03 +0000
committerGravatar Stefan Monnier <monnier@iro.umontreal.ca>2014-06-06 17:23:03 +0000
commitb9c06ced8e899854d06314b52d0182e123775afc (patch)
tree588fbaf256bcdcb8b8b7d889ed34538f8f7083f4 /coq/ex
parent1c0b0d32f95d7555943ab86a2de6666e39e84c13 (diff)
* coq/coq-smie.el: Fix precedence of 'else'.
Diffstat (limited to 'coq/ex')
-rw-r--r--coq/ex/indent.v6
1 files changed, 6 insertions, 0 deletions
diff --git a/coq/ex/indent.v b/coq/ex/indent.v
index c452cd1b..7218fa63 100644
--- a/coq/ex/indent.v
+++ b/coq/ex/indent.v
@@ -40,6 +40,12 @@ Proof.
}}
Qed.
+Let x (* Precedence of "else" w.r.t "," and "->"! *)
+ : if true then nat * nat else nat ->
+ nat
+ := (if true then 1 else 2,
+ 3).
+
Module Y.
Lemma L : forall x:nat , nat_iter x (A:=nat) (plus 2) 0 >= x.
Proof with auto with arith.