Fix first two suggestions in Issue cpitclaudel#254

This PR is to fix the first two suggestions made in Issue cpitclaudel#254. I also encountered these issues when going through the tutorial.
guojing0 · Mar 11, 2023 · c391f6e · c391f6e
1 parent 5affe7a
commit c391f6e
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/refman/tutorial.v b/refman/tutorial.v
@@ -115,7 +115,7 @@ Ltac MySimpleTactic :=
     and adjusts completions accordingly *)
 
 (* Run the following snippet, then try typing ‘plus’ *)
-SearchAbout eq.
+Search eq.
 
 
 (******************************************************************************)
@@ -138,8 +138,8 @@ Abort.
    key down.  Release the mouse button to hide the info box.  This also works
    without a graphic environment; just enable ‘xterm-mouse-mode’ (alternatively,
    you can use the ‘<menu>’ key, or even ‘M-F12’). *)
-Fail le.
-Fail exfalso.
+Print le.
+Print exfalso.
 
 (******************************************************************************)