aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder/rules.ml
diff options
context:
space:
mode:
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 8c6b5b91d..f745dbeb4 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) ||