fix typo

coq · Aug 26, 2024 · 48f5224 · 48f5224
1 parent 7068ffc
commit 48f5224
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/Tutorial_SSReflect_tactics.v b/src/Tutorial_SSReflect_tactics.v
@@ -160,9 +160,9 @@ revert P Q HP HQ.
 generalize or_comm.
 Abort.
 
-(*
+(**
   One goes from a goal of the form [P] to [T -> P] where [T] is a result from the global context.
-  If one look at the goal only, it seems that it has been weakened.
+  If one looks at the goal only, it seems that it has been weakened.
   However, it is indeed a generalisation and here follows an explanation why.
 
   One should look at the whole information that consists of both the context and the goal.