Imported Upstream version 8.6upstream/8.6

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