diff options
| author |  Julien Forest <julien.forest@ensiie.fr> | 2014-02-14 14:52:56 +0100 |
|---|---|---|
| committer | Julien Forest <julien.forest@ensiie.fr> | 2014-02-14 14:52:56 +0100 |
| commit | f4d6b4bce315639008b52727f741de82e2687d7e (patch) | |
| tree | 7bed389e46faa9971e06b0c9fb826c620809dd85 | |
| parent | 85f1d9ca4b10a80be6929c81e2e6ca4c7634f619 (diff) | |
fast correction of bug #3234
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 26e1011ba..f951debfd 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -278,7 +278,7 @@ let tclUSER tac is_mes l g = let tclUSER_if_not_mes concl_tac is_mes names_to_suppress = if is_mes then tclCOMPLETE (Simple.apply (delayed_force well_founded_ltof)) - else tclTHEN (Simple.apply (delayed_force acc_intro_generator_function) ) (tclUSER concl_tac is_mes names_to_suppress) + else (* tclTHEN (Simple.apply (delayed_force acc_intro_generator_function) ) *) (tclUSER concl_tac is_mes names_to_suppress) |