diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 3 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 6 |
4 files changed, 9 insertions, 8 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 169a706005..c9dd18a2fc 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -52,10 +52,10 @@ let rec print_debug_queue e = let _ = match e with | Some e -> - Pp.msg_debug (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal) + Pp.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal)) | None -> begin - Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal); + Pp.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal); end in print_debug_queue None ; end diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index eadeebd38e..ab3629f89e 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -10,6 +10,7 @@ open Glob_term open Declarations open Misctypes open Decl_kinds +open Sigma.Notations let is_rec_info scheme_info = let test_branche min acc (_,_,br) = @@ -86,7 +87,7 @@ let functional_induction with_clean c princl pat = in let encoded_pat_as_patlist = List.make (List.length args + List.length c_list - 1) None @ [pat] in - List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr (fun env sigma -> sigma,(c,NoBindings))),(None,pat),None)) + List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr ({ Tacexpr.delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) })),(None,pat),None)) (args@c_list) encoded_pat_as_patlist in let princ' = Some (princ,bindings) in diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index d979401424..d074bbabd8 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -70,8 +70,8 @@ let do_observe_tac s tac g = with reraise -> let reraise = Errors.push reraise in let e = Cerrors.process_vernac_interp_error reraise in - observe (str "observation "++ s++str " raised exception " ++ - Errors.iprint e ++ str " on goal " ++ goal ); + observe (hov 0 (str "observation "++ s++str " raised exception " ++ + Errors.iprint e ++ str " on goal" ++ fnl() ++ goal )); iraise reraise;; diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index ca0b9c5feb..aaeb577d39 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] |