diff options
| author | Maxime Dénès | 2017-06-06 00:24:57 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-06 00:24:57 +0200 |
| commit | cc0f9d254c394db742473299336fb20b82ae4aa1 (patch) | |
| tree | cbc89906c862624d4285f367d1fa9f0f61f16f05 /plugins/quote | |
| parent | b377bd30f23f430882902f534eaf31b1314ecd07 (diff) | |
| parent | 88fdd28815747520bdc555a2d1b8600e114ab341 (diff) | |
Merge PR#716: Don't double up on periods in anomalies
Diffstat (limited to 'plugins/quote')
| -rw-r--r-- | plugins/quote/quote.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index ba8356b525..59ed8439b6 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -423,7 +423,7 @@ let quote_terms env sigma ivs lc = | None -> begin match ivs.constant_lhs with | Some c_lhs -> subst_meta [1, c] c_lhs - | None -> anomaly (Pp.str "invalid inversion scheme for quote") + | None -> anomaly (Pp.str "invalid inversion scheme for quote.") end | Some var_lhs -> begin match ivs.constant_lhs with |