diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 3 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 1 | ||||
| -rw-r--r-- | plugins/rtauto/proof_search.ml | 4 | ||||
| -rw-r--r-- | plugins/rtauto/proof_search.mli | 2 |
4 files changed, 4 insertions, 6 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 13b3dabdf8..4d5cbe2232 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1415,7 +1415,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic = (* let ids = List.filter (fun id -> not (List.mem id ids)) ids' in *) (* rewrite *) (* ) *) - Eauto.gen_eauto false (false,5) [] (Some []) + Eauto.gen_eauto (false,5) [] (Some []) ] gls @@ -1493,7 +1493,6 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = ( tclCOMPLETE( Eauto.eauto_with_bases - false (true,5) [Evd.empty,Lazy.force refl_equal] [Auto.Hint_db.empty empty_transparent_state false] diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 7613c6765f..8eb7d0e8fc 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1322,7 +1322,6 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings)) e_assumption; Eauto.eauto_with_bases - false (true,5) [Evd.empty,Lazy.force refl_equal] [Auto.Hint_db.empty empty_transparent_state false] diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 2448a2d393..d772279f10 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -510,8 +510,8 @@ let pp_gl gl= cut () ++ let pp = function - Incomplete(gl,ctx) -> msgnl (pp_gl gl) - | _ -> msg (str "<complete>") + Incomplete(gl,ctx) -> pp_gl gl ++ fnl () + | _ -> str "<complete>" let pp_info () = let count_info = diff --git a/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli index b236aa7215..275e94cde5 100644 --- a/plugins/rtauto/proof_search.mli +++ b/plugins/rtauto/proof_search.mli @@ -38,7 +38,7 @@ val branching: state -> state list val success: state -> bool -val pp: state -> unit +val pp: state -> Pp.std_ppcmds val pr_form : form -> unit |