aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/recdef.ml
diff options
context:
space:
mode:
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