Add some missing Proof statements.

2 files changed, 3 insertions, 2 deletions

diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index 7d7dcc6d0..746161b38 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -34,6 +34,7 @@ Definition shift (c : bool) (a : ascii) :=
 (** Definition of a decidable function that is effective *)
 
 Definition ascii_dec : forall a b : ascii, {a = b} + {a <> b}.
+Proof.
   decide equality; apply bool_dec.
 Defined.
 
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index 6294d156b..1479695d8 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -29,6 +29,7 @@ Local Open Scope string_scope.
 (** Equality is decidable *)
 
 Definition string_dec : forall s1 s2 : string, {s1 = s2} + {s1 <> s2}.
+Proof.
  decide equality; apply ascii_dec.
 Defined.
 
@@ -41,7 +42,6 @@ Fixpoint append (s1 s2 : string) : string :=
   | EmptyString => s2
   | String c s1' => String c (s1' ++ s2)
   end
-
 where "s1 ++ s2" := (append s1 s2) : string_scope.
 
 (******************************)
@@ -379,7 +379,7 @@ Definition findex n s1 s2 :=
 (**
   The concrete syntax for strings in scope string_scope follows the
   Coq convention for strings: all ascii characters of code less than
-  128 are litteral to the exception of the character `double quote'
+  128 are literals to the exception of the character `double quote'
   which must be doubled.
 
   Strings that involve ascii characters of code >= 128 which are not