aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2018-02-07 17:17:56 +0100
committerGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2018-02-07 17:17:56 +0100
commita3c3f5dc3dae5354ccb618335a0bcd4920655b42 (patch)
tree2f346300be3eff9e5de510b1c234b9c4759a09d8
parent945cada601c5729edd16fcc989a3969c8b34d20a (diff)
typo in abbrevs.
-rw-r--r--coq/coq-syntax.el2
1 files changed, 1 insertions, 1 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 156d39e1..5b55126c 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -516,7 +516,7 @@ so for the following reasons:
("Instance goal" "instg" "Instance #:#.\n#\nDefined." t);; careful
("Lemma" "l" "Lemma # : #.\nProof.\n#\nQed." t "Lemma")
("Program Lemma" "pl" "Program Lemma # : #.\nProof.\n#\nQed." t "Program\\s-+Lemma")
- ("Proposition" "l" "Proposition # : #.\nProof.\n#\nQed." t "Proposition")
+ ("Proposition" "pr" "Proposition # : #.\nProof.\n#\nQed." t "Proposition")
("Module! (interactive)" nil "Module # : #.\n#\nEnd #." nil nil coq-insert-section-or-module)
("Module Type" "mti" "Module Type #.\n#\nEnd #." t "Module\\s-+Type") ; careful
("Module :" "moi" "Module # : #.\n#\nEnd #." t "Module") ; careful