diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /plugins/rtauto | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'plugins/rtauto')
-rw-r--r-- | plugins/rtauto/Bintree.v | 2 | ||||
-rw-r--r-- | plugins/rtauto/proof_search.ml | 4 | ||||
-rw-r--r-- | plugins/rtauto/refl_tauto.ml | 29 | ||||
-rw-r--r-- | plugins/rtauto/refl_tauto.mli | 2 | ||||
-rw-r--r-- | plugins/rtauto/rtauto_plugin.mlpack (renamed from plugins/rtauto/rtauto_plugin.mllib) | 1 |
5 files changed, 19 insertions, 19 deletions
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.mlpack index 0e346044..61c5e945 100644 --- a/plugins/rtauto/rtauto_plugin.mllib +++ b/plugins/rtauto/rtauto_plugin.mlpack @@ -1,4 +1,3 @@ Proof_search Refl_tauto G_rtauto -Rtauto_plugin_mod |