From d5b07336d9e4d94a5b4369c032afd30ecc084411 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 22 Sep 2016 07:29:02 -0700 Subject: [PATCH] chore(emacs): use \pr for projection notation --- src/emacs/lean-input.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/emacs/lean-input.el b/src/emacs/lean-input.el index a898427fde..6a5ccc2670 100644 --- a/src/emacs/lean-input.el +++ b/src/emacs/lean-input.el @@ -233,7 +233,7 @@ order for the change to take effect." ("pequiv" . ("≃*")) ("phomotopy" . ("~*")) - ("p" . ("↣")) + ("pr" . ("↣")) ("1" . ("₁")) ("2" . ("₂"))