From 64ea715e48b14ec8a793453b76db332e032d5cb0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 18 Jan 2020 11:51:48 +0100
Subject: Reference manual: Typos/English in chapter universe polymorphism.

---
 doc/sphinx/addendum/universe-polymorphism.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 7adb25cbd6..f9cc25959c 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -529,8 +529,8 @@ sections, except in the following ways:
        Polymorphic Universe i.
        Fail Constraint i = i.
 
-  This includes constraints implictly declared by commands such as
-  :cmd:`Variable`, which may as a such need to be used with universe
+  This includes constraints implicitly declared by commands such as
+  :cmd:`Variable`, which may need to be used with universe
   polymorphism activated (locally by attribute or globally by option):
 
   .. coqtop:: all
-- 
cgit v1.2.3


From 7e98fc9ee477505e3bb6d2c91a3d5d46d5fffbc5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 20 Jan 2020 08:45:18 +0100
Subject: Typo in a comment of univ.mli.

---
 kernel/univ.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/kernel/univ.mli b/kernel/univ.mli
index 1914ce5e34..f7c984870f 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -322,7 +322,7 @@ val in_punivs : 'a -> 'a puniverses
 val eq_puniverses : ('a -> 'a -> bool) -> 'a puniverses -> 'a puniverses -> bool
 
 (** A vector of universe levels with universe Constraint.t,
-    representiong local universe variables and associated Constraint.t *)
+    representing local universe variables and associated Constraint.t *)
 
 module UContext :
 sig
-- 
cgit v1.2.3


From 9d88395fd25031445d463648e81c600df179cbc6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 20 Jan 2020 08:45:35 +0100
Subject: Typo in an anomaly message.

---
 vernac/declareUniv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml
index 69ba9d76ec..def2fdad2a 100644
--- a/vernac/declareUniv.ml
+++ b/vernac/declareUniv.ml
@@ -72,7 +72,7 @@ let declare_univ_binders gr pl =
         CErrors.anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".")
       | ConstructRef _ ->
         CErrors.anomaly ~label:"declare_univ_binders"
-          Pp.(str "declare_univ_binders on an constructor reference")
+          Pp.(str "declare_univ_binders on a constructor reference")
     in
     let univs = Id.Map.fold (fun id univ univs ->
         match Univ.Level.name univ with
-- 
cgit v1.2.3


From 61afb01b721d12068ade37f5c809319668e3573e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 20 Jan 2020 08:45:51 +0100
Subject: Translating a comment from French to English.

---
 tactics/declare.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/declare.ml b/tactics/declare.ml
index da4de3df77..9a14f4d40f 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -362,7 +362,7 @@ let inVariable : unit -> obj =
     classify_function = (fun () -> Dispose)}
 
 let declare_variable ~name ~kind d =
-  (* Constr raisonne sur les noms courts *)
+  (* Variables are distinguished by only short names *)
   if Decls.variable_exists name then
     raise (AlreadyDeclared (None, name));
 
-- 
cgit v1.2.3