From f4d6b4bce315639008b52727f741de82e2687d7e Mon Sep 17 00:00:00 2001 From: Julien Forest Date: Fri, 14 Feb 2014 14:52:56 +0100 Subject: fast correction of bug #3234 --- plugins/funind/recdef.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind/recdef.ml') 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) -- cgit v1.2.3