diff options
Diffstat (limited to 'plugins/rtauto/proof_search.ml')
| -rw-r--r-- | plugins/rtauto/proof_search.ml | 29 |
1 files changed, 15 insertions, 14 deletions
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 8b926111..3de59239 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors @@ -46,8 +48,7 @@ let reset_info () = let pruning = ref true let opt_pruning= - {optsync=true; - optdepr=false; + {optdepr=false; optname="Rtauto Pruning"; optkey=["Rtauto";"Pruning"]; optread=(fun () -> !pruning); @@ -146,7 +147,7 @@ let add_step s sub = | SI_Or_r,[p] -> I_Or_r p | SE_Or i,[p1;p2] -> E_Or(i,p1,p2) | SD_Or i,[p] -> D_Or(i,p) - | _,_ -> anomaly ~label:"add_step" (Pp.str "wrong arity") + | _,_ -> anomaly ~label:"add_step" (Pp.str "wrong arity.") type 'a with_deps = {dep_it:'a; @@ -168,7 +169,7 @@ type state = let project = function Complete prf -> prf - | Incomplete (_,_) -> anomaly (Pp.str "not a successful state") + | Incomplete (_,_) -> anomaly (Pp.str "not a successful state.") let pop n prf = let nprf= @@ -362,7 +363,7 @@ let search_norev seq= (Arrow(f2,f3))) f1; add_hyp (embed nseq) f3]):: !goals - | _ -> anomaly ~label:"search_no_rev" (Pp.str "can't happen") in + | _ -> anomaly ~label:"search_no_rev" (Pp.str "can't happen.") in Int.Map.iter add_one seq.norev_hyps; List.rev !goals @@ -387,7 +388,7 @@ let search_in_rev_hyps seq= | Arrow (Disjunct (f1,f2),f0) -> [make_step (SD_Or(i)), [add_hyp (add_hyp (embed nseq) (Arrow(f1,f0))) (Arrow (f2,f0))]] - | _ -> anomaly ~label:"search_in_rev_hyps" (Pp.str "can't happen") + | _ -> anomaly ~label:"search_in_rev_hyps" (Pp.str "can't happen.") with Not_found -> search_norev seq @@ -465,7 +466,7 @@ let branching = function | _::next -> s_info.nd_branching<-s_info.nd_branching+List.length next in List.map (append stack) successors - | Complete prf -> anomaly (Pp.str "already succeeded") + | Complete prf -> anomaly (Pp.str "already succeeded.") open Pp @@ -505,12 +506,12 @@ let pp_mapint map = pp_form obj ++ str " => " ++ pp_list (fun (i,f) -> pp_form f) l ++ cut ()) ) map; - str "{ " ++ vb 0 ++ (!pp) ++ str " }" ++ close () + str "{ " ++ hv 0 (!pp ++ str " }") let pp_connect (i,j,f1,f2) = pp_form f1 ++ str " => " ++ pp_form f2 let pp_gl gl= cut () ++ - str "{ " ++ vb 0 ++ + str "{ " ++ hv 0 ( begin match gl.abs with None -> str "" @@ -520,7 +521,7 @@ let pp_gl gl= cut () ++ str "norev =" ++ pp_intmap gl.norev_hyps ++ cut () ++ str "arrows=" ++ pp_mapint gl.right ++ cut () ++ str "cnx =" ++ pp_list pp_connect gl.cnx ++ cut () ++ - str "goal =" ++ pp_form gl.gl ++ str " }" ++ close () + str "goal =" ++ pp_form gl.gl ++ str " }") let pp = function |