From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- plugins/rtauto/Bintree.v | 2 +- plugins/rtauto/proof_search.ml | 4 ++-- plugins/rtauto/refl_tauto.ml | 29 +++++++++++++++-------------- plugins/rtauto/refl_tauto.mli | 2 +- plugins/rtauto/rtauto_plugin.mllib | 4 ---- plugins/rtauto/rtauto_plugin.mlpack | 3 +++ 6 files changed, 22 insertions(+), 22 deletions(-) delete mode 100644 plugins/rtauto/rtauto_plugin.mllib create mode 100644 plugins/rtauto/rtauto_plugin.mlpack (limited to 'plugins/rtauto') diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v index 7394cebd..36460187 100644 --- a/plugins/rtauto/Bintree.v +++ b/plugins/rtauto/Bintree.v @@ -266,7 +266,7 @@ Qed. Lemma push_not_empty: forall a S, (push a S) <> empty. intros a [ind cont];unfold push,empty. -simpl;intro H;injection H; intros _ ; apply Pos.succ_not_1. +intros [= H%Pos.succ_not_1]. assumption. Qed. Fixpoint In (x:A) (S:Store) (F:Full S) {struct F}: Prop := diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 3ba92b9f..8b926111 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Goptions @@ -547,7 +547,7 @@ let pp_info () = int s_info.created_branches ++ str " created" ++ fnl () ++ str "Hypotheses : " ++ int s_info.created_hyps ++ str " created" ++ fnl () in - msg_info + Feedback.msg_info ( str "Proof-search statistics :" ++ fnl () ++ count_info ++ str "Branch ends: " ++ diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 9c22b5ad..4ed90795 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -8,11 +8,12 @@ module Search = Explore.Make(Proof_search) -open Errors +open CErrors open Util open Term open Tacmach open Proof_search +open Context.Named.Declaration let force count lazc = incr count;Lazy.force lazc @@ -66,12 +67,12 @@ let l_D_Or = lazy (constant "D_Or") let special_whd gl= - let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in - (fun t -> Closure.whd_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in + (fun t -> CClosure.whd_val infos (CClosure.inject t)) let special_nf gl= - let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in - (fun t -> Closure.norm_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in + (fun t -> CClosure.norm_val infos (CClosure.inject t)) type atom_env= {mutable next:int; @@ -128,9 +129,9 @@ let rec make_form atom_env gls term = let rec make_hyps atom_env gls lenv = function [] -> [] - | (_,Some body,typ)::rest -> + | LocalDef (_,body,typ)::rest -> make_hyps atom_env gls (typ::body::lenv) rest - | (id,None,typ)::rest -> + | LocalAssum (id,typ)::rest -> let hrec= make_hyps atom_env gls (typ::lenv) rest in if List.exists (Termops.dependent (mkVar id)) lenv || @@ -275,7 +276,7 @@ let rtauto_tac gls= begin reset_info (); if !verbose then - msg_info (str "Starting proof-search ..."); + Feedback.msg_info (str "Starting proof-search ..."); end in let search_start_time = System.get_time () in let prf = @@ -285,10 +286,10 @@ let rtauto_tac gls= let search_end_time = System.get_time () in let _ = if !verbose then begin - msg_info (str "Proof tree found in " ++ + Feedback.msg_info (str "Proof tree found in " ++ System.fmt_time_difference search_start_time search_end_time); pp_info (); - msg_info (str "Building proof term ... ") + Feedback.msg_info (str "Building proof term ... ") end in let build_start_time=System.get_time () in let _ = step_count := 0; node_count := 0 in @@ -301,7 +302,7 @@ let rtauto_tac gls= let build_end_time=System.get_time () in let _ = if !verbose then begin - msg_info (str "Proof term built in " ++ + Feedback.msg_info (str "Proof term built in " ++ System.fmt_time_difference build_start_time build_end_time ++ fnl () ++ str "Proof size : " ++ int !step_count ++ @@ -315,12 +316,12 @@ let rtauto_tac gls= if !check then Proofview.V82.of_tactic (Tactics.exact_check term) gls else - Tactics.exact_no_check term gls in + Proofview.V82.of_tactic (Tactics.exact_no_check term) gls in let tac_end_time = System.get_time () in let _ = - if !check then msg_info (str "Proof term type-checking is on"); + if !check then Feedback.msg_info (str "Proof term type-checking is on"); if !verbose then - msg_info (str "Internal tactic executed in " ++ + Feedback.msg_info (str "Internal tactic executed in " ++ System.fmt_time_difference tac_start_time tac_end_time) in result diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli index c9e591bb..9a14ac6c 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -18,7 +18,7 @@ val make_hyps : atom_env -> Proof_type.goal Tacmach.sigma -> Term.types list -> - (Names.Id.t * Term.types option * Term.types) list -> + Context.Named.t -> (Names.Id.t * Proof_search.form) list val rtauto_tac : Proof_type.tactic diff --git a/plugins/rtauto/rtauto_plugin.mllib b/plugins/rtauto/rtauto_plugin.mllib deleted file mode 100644 index 0e346044..00000000 --- a/plugins/rtauto/rtauto_plugin.mllib +++ /dev/null @@ -1,4 +0,0 @@ -Proof_search -Refl_tauto -G_rtauto -Rtauto_plugin_mod diff --git a/plugins/rtauto/rtauto_plugin.mlpack b/plugins/rtauto/rtauto_plugin.mlpack new file mode 100644 index 00000000..61c5e945 --- /dev/null +++ b/plugins/rtauto/rtauto_plugin.mlpack @@ -0,0 +1,3 @@ +Proof_search +Refl_tauto +G_rtauto -- cgit v1.2.3