diff options
| author |  Assia Mahboubi <assia.mahboubi@inria.fr> | 2007-12-07 15:18:12 +0000 |
|---|---|---|
| committer | Assia Mahboubi <assia.mahboubi@inria.fr> | 2007-12-07 15:18:12 +0000 |
| commit | 8f0e60934c205b4fdba26c1e205988dca92bd02c (patch) | |
| tree | ea7cdcce2bd2d925c540294863a1e24367d7a84f /coq | |
| parent | da21b5e16c55b9e8242cae9035b34a5d6c58c5af (diff) | |
Print Coercions added to coq-syntax
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-syntax.el | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 1aa5c65d..33c4e6c3 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -532,6 +532,7 @@ so for the following reasons: ("Obligations Tactic" nil "Obligations Tactic := #." t "Obligations\\s-+Tactic") ("Open Local Scope" "oplsc" "Open Local Scope #" t "Open\\s-+Local\\s-+Scope") ("Open Scope" "opsc" "Open Scope #" t "Open\\s-+Scope") + ("Print Coercions" nil "Print Coercions." nil "Print\\s-+Coercions") ("Print Hint" nil "Print Hint." nil "Print\\s-+Hint" coq-PrintHint) ("Print" "p" "Print #." nil "Print") ("Qed" nil "Qed." nil "Qed") |