diff options
| -rw-r--r-- | plugins/funind/recdef.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index c42ecac42..057ffb9b3 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1425,6 +1425,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let hook _ _ = let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in + let _ = Table.extraction_inline true [Ident (dummy_loc,term_id)] in (* message "start second proof"; *) let stop = ref false in begin |