diff --git a/ide/coqide.ml b/ide/coqide.ml
index aa9e150fd50c..4f00be27a1d6 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -561,7 +561,7 @@ let update_status sn =
       | None -> ""
       | Some n -> ", proving " ^ n
     in
-    display ("Ready"^ (if nanoPG#get then ", [μPG]" else "") ^ path ^ name);
+    display ("Ready"^ (if microPG#get then ", [μPG]" else "") ^ path ^ name);
     Coq.return ()
   in
   Coq.bind (Coq.status false) next
@@ -1200,7 +1200,7 @@ let build_ui () =
     item "Help for μPG mode" ~label:"Help for μPG mode"
       ~callback:(fun _ -> on_current_term (fun sn ->
          sn.messages#default_route#clear;
-         sn.messages#default_route#add_string (NanoPG.get_documentation ())));
+         sn.messages#default_route#add_string (MicroPG.get_documentation ())));
     item "About Coq" ~label:"_About" ~stock:`ABOUT
       ~callback:MiscMenu.about
   ];
@@ -1234,7 +1234,7 @@ let build_ui () =
   let () = vbox#pack toolbar#coerce in
 
   (* Emacs/PG mode *)
-  NanoPG.init w notebook all_menus;
+  MicroPG.init w notebook all_menus;
 
   (* On tab switch, reset, update location *)
   let _ = notebook#connect#switch_page ~callback:(fun n ->
@@ -1251,7 +1251,7 @@ let build_ui () =
   let () = refresh_notebook_pos () in
   let lower_hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in
   let () = lower_hbox#pack ~expand:true status#coerce in
-  let () = push_info ("Ready"^ if nanoPG#get then ", [μPG]" else "")  in
+  let () = push_info ("Ready"^ if microPG#get then ", [μPG]" else "")  in
 
   (* Location display *)
   let l = GMisc.label
diff --git a/ide/ide.mllib b/ide/ide.mllib
index ed6520f29f59..f8e8ff48d619 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -30,5 +30,5 @@ CoqOps
 Wg_Command
 Session
 Coqide_ui
-NanoPG
+MicroPG
 Coqide
diff --git a/ide/nanoPG.ml b/ide/microPG.ml
similarity index 99%
rename from ide/nanoPG.ml
rename to ide/microPG.ml
index 5e6c0b846279..25cab4638cb0 100644
--- a/ide/nanoPG.ml
+++ b/ide/microPG.ml
@@ -325,7 +325,7 @@ let init w nb ags =
     then false
     else begin
     eprintf "got key %s\n%!" (pr_key t);
-    if nanoPG#get then begin
+    if microPG#get then begin
       match find gui !cur t with
       | `Do e ->
            eprintf "run (%s) %s on %s\n%!" e.keyname e.doc (pr_status !status);
diff --git a/ide/nanoPG.mli b/ide/microPG.mli
similarity index 100%
rename from ide/nanoPG.mli
rename to ide/microPG.mli
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 3893d023bdd6..4e2e3f31e6e6 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -561,7 +561,8 @@ let tab_length =
 let highlight_current_line =
   new preference ~name:["highlight_current_line"] ~init:false ~repr:Repr.(bool)
 
-let nanoPG =
+let microPG =
+  (* Legacy name in preference is "nanoPG" *)
   new preference ~name:["nanoPG"] ~init:false ~repr:Repr.(bool)
 
 let user_queries =
@@ -799,7 +800,7 @@ let configure ?(apply=(fun () -> ())) parent =
     let () = button "Show progress bar" show_progress_bar in
     let () = button "Insert spaces instead of tabs" spaces_instead_of_tabs in
     let () = button "Highlight current line" highlight_current_line in
-    let () = button "Emacs/PG keybindings (μPG mode)" nanoPG in
+    let () = button "Emacs/PG keybindings (μPG mode)" microPG in
     let callback () = () in
     custom ~label box callback true
   in
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 785c191b46d9..b01c4598d8f0 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -102,7 +102,7 @@ val show_progress_bar : bool preference
 val spaces_instead_of_tabs : bool preference
 val tab_length : int preference
 val highlight_current_line : bool preference
-val nanoPG : bool preference
+val microPG : bool preference
 val user_queries : (string * string) list preference
 val diffs : string preference