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(-)

(limited to 'vernac/declareUniv.ml')

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