aboutsummaryrefslogtreecommitdiff
path: root/plugins/rtauto
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/rtauto')
-rw-r--r--plugins/rtauto/Bintree.v4
-rw-r--r--plugins/rtauto/Rtauto.v2
-rw-r--r--plugins/rtauto/g_rtauto.ml42
-rw-r--r--plugins/rtauto/proof_search.ml6
-rw-r--r--plugins/rtauto/proof_search.mli2
-rw-r--r--plugins/rtauto/refl_tauto.ml35
-rw-r--r--plugins/rtauto/refl_tauto.mli4
-rw-r--r--plugins/rtauto/rtauto_plugin.mlpack (renamed from plugins/rtauto/rtauto_plugin.mllib)1
8 files changed, 28 insertions, 28 deletions
diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index 267cd47233..3646018719 100644
--- a/plugins/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -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/Rtauto.v b/plugins/rtauto/Rtauto.v
index 61a160b2cc..0dc6e31b85 100644
--- a/plugins/rtauto/Rtauto.v
+++ b/plugins/rtauto/Rtauto.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4
index 7fefab3ed0..d27b04834e 100644
--- a/plugins/rtauto/g_rtauto.ml4
+++ b/plugins/rtauto/g_rtauto.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 23510117b1..8b92611136 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * 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/proof_search.mli b/plugins/rtauto/proof_search.mli
index 86a2fb666b..31f8e7b51d 100644
--- a/plugins/rtauto/proof_search.mli
+++ b/plugins/rtauto/proof_search.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 4ffc1f3318..367a133330 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -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 ||
@@ -262,7 +263,7 @@ let rtauto_tac gls=
let _=
if Retyping.get_sort_family_of
(pf_env gls) (Tacmach.project gls) gl != InProp
- then errorlabstrm "rtauto" (Pp.str "goal should be in Prop") in
+ then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in
let glf=make_form gamma gls gl in
let hyps=make_hyps gamma gls [gl] (pf_hyps gls) in
let formula=
@@ -275,20 +276,20 @@ 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 =
try project (search_fun (init_state [] formula))
with Not_found ->
- errorlabstrm "rtauto" (Pp.str "rtauto couldn't find any proof") in
+ user_err ~hdr:"rtauto" (Pp.str "rtauto couldn't find any proof") in
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 45fb50dcca..9a14ac6c79 100644
--- a/plugins/rtauto/refl_tauto.mli
+++ b/plugins/rtauto/refl_tauto.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -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 0e34604495..61c5e945bc 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 10:12:53 +0000