diff options
| author | Hugo Herbelin | 2020-01-20 08:45:35 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-01-21 00:20:49 +0100 |
| commit | 9d88395fd25031445d463648e81c600df179cbc6 (patch) | |
| tree | 45dcb8adee2088a034ade2af398bb5c79f93485b /vernac/declareUniv.ml | |
| parent | 7e98fc9ee477505e3bb6d2c91a3d5d46d5fffbc5 (diff) | |
Typo in an anomaly message.
Diffstat (limited to 'vernac/declareUniv.ml')
| -rw-r--r-- | vernac/declareUniv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |