aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/recdef.ml
diff options
context:
space:
mode:
authorJPR2019-05-22 21:40:57 +0200
committerThéo Zimmermann2019-05-23 01:49:04 +0200
commit467eb67bb960c15e1335f375af29b4121ac5262b (patch)
tree1ad2454c535b090738748cd8123330451a498854 /plugins/funind/recdef.ml
parent20a464396fd89449569dc69b8cfb37cb69766733 (diff)
Fixing typos - Part 2
Diffstat (limited to 'plugins/funind/recdef.ml')
-rw-r--r--plugins/funind/recdef.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 1fca132655..216be3797b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1584,7 +1584,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
spc () ++ str"is defined" )
)
in
- (* XXX STATE Why do we need this... why is the toplevel protection not enought *)
+ (* XXX STATE Why do we need this... why is the toplevel protection not enough *)
funind_purify (fun () ->
let pstate = com_terminate
tcc_lemma_name