aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder/rules.ml
diff options
context:
space:
mode:
authorMaxime Dénès2017-06-06 00:24:57 +0200
committerMaxime Dénès2017-06-06 00:24:57 +0200
commitcc0f9d254c394db742473299336fb20b82ae4aa1 (patch)
treecbc89906c862624d4285f367d1fa9f0f61f16f05 /plugins/firstorder/rules.ml
parentb377bd30f23f430882902f534eaf31b1314ecd07 (diff)
parent88fdd28815747520bdc555a2d1b8600e114ab341 (diff)
Merge PR#716: Don't double up on periods in anomalies
Diffstat (limited to 'plugins/firstorder/rules.ml')
-rw-r--r--plugins/firstorder/rules.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 8c6b5b91de..f745dbeb4b 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -40,7 +40,7 @@ let wrap n b continue seq =
let rec aux i nc ctx=
if i<=0 then seq else
match nc with
- []->anomaly (Pp.str "Not the expected number of hyps")
+ []->anomaly (Pp.str "Not the expected number of hyps.")
| nd::q->
let id = NamedDecl.get_id nd in
if occur_var env sigma id (pf_concl gls) ||