diff options
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 5d41ec7237..685a5e8bdf 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -212,10 +212,10 @@ let rec print_debug_queue b e = begin let lmsg,goal = Stack.pop debug_queue in if b then - Pp.msg_debug (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal) + Pp.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal)) else begin - Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal); + Pp.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal)); end; (* print_debug_queue false e; *) end @@ -1327,7 +1327,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp tclFIRST[ tclTHEN (Proofview.V82.of_tactic (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))) - e_assumption; + (Proofview.V82.of_tactic e_assumption); Eauto.eauto_with_bases (true,5) [Evd.empty,Lazy.force refl_equal] |