aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/recdef.ml
diff options
context:
space:
mode:
authorThéo Zimmermann2019-05-23 15:10:20 +0200
committerThéo Zimmermann2019-05-23 15:10:20 +0200
commite7628797fc241a4d7a5c1a5675cb679db282050d (patch)
tree8e8cc4348dfb9247713f45a7c43668ba98c708cf /plugins/funind/recdef.ml
parentcf3b9eca0b3e81a7d56acded394a8b6843a4bb8d (diff)
parent467eb67bb960c15e1335f375af29b4121ac5262b (diff)
Merge PR #10221: Fixing typos - Part 2 (reopening of #10218)
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