Imported Upstream version 8.5~beta1+dfsg

7 files changed, 115 insertions, 107 deletions

diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index fbfa1bfd..267cd472 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-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -198,7 +198,7 @@ Theorem get_Full_Gt : forall S, Full S ->
 Proof.
 intros S W;induction W.
 unfold empty,index,get,contents;intros;apply Tget_Tempty.
-unfold index,get,push;simpl contents.
+unfold index,get,push. simpl @contents.
 intros i e;rewrite Tget_Tadd.
 rewrite (Gt_Psucc _ _ e).
 unfold get in IHW.
@@ -209,7 +209,7 @@ Theorem get_Full_Eq : forall S, Full S -> get (index S) S = PNone.
 intros [index0 contents0] F.
 case F.
 unfold empty,index,get,contents;intros;apply Tget_Tempty.
-unfold index,get,push;simpl contents.
+unfold push,index,get;simpl @contents.
 intros a S.
 rewrite Tget_Tadd.
 rewrite Psucc_Gt.
@@ -231,12 +231,12 @@ Proof.
 intros i a S F.
 case_eq (i ?= index S).
 intro e;rewrite (Pos.compare_eq _ _ e).
-destruct S;unfold get,push,index;simpl contents;rewrite Tget_Tadd.
+destruct S;unfold get,push,index;simpl @contents;rewrite Tget_Tadd.
 rewrite Pos.compare_refl;reflexivity.
-intros;destruct S;unfold get,push,index;simpl contents;rewrite Tget_Tadd.
-simpl index in H;rewrite H;reflexivity.
+intros;destruct S;unfold get,push,index;simpl @contents;rewrite Tget_Tadd.
+simpl @index in H;rewrite H;reflexivity.
 intro H;generalize H;clear H.
-unfold get,push;simpl index;simpl contents.
+unfold get,push;simpl.
 rewrite Tget_Tadd;intro e;rewrite e.
 change (get i S=PNone).
 apply get_Full_Gt;auto.
@@ -260,7 +260,7 @@ Qed.
 Lemma Full_index_one_empty : forall S, Full S -> index S = 1 -> S=empty.
 intros [ind cont] F one; inversion F.
 reflexivity.
-simpl index in one;assert (h:=Pos.succ_not_1 (index S)).
+simpl @index in one;assert (h:=Pos.succ_not_1 (index S)).
 congruence.
 Qed.
 
diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v
index f823cf74..61a160b2 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-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \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 4de2638b..7fefab3e 100644
--- a/plugins/rtauto/g_rtauto.ml4
+++ b/plugins/rtauto/g_rtauto.ml4
@@ -1,14 +1,16 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "parsing/grammar.cma"  i*)
+(*i camlp4deps: "grammar/grammar.cma"  i*)
+
+DECLARE PLUGIN "rtauto_plugin"
 
 TACTIC EXTEND rtauto
-  [ "rtauto" ] -> [ Refl_tauto.rtauto_tac ]
+  [ "rtauto" ] -> [ Proofview.V82.tactic (Refl_tauto.rtauto_tac) ]
 END
 
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 2ace38bd..23510117 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-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
+open Errors
 open Util
 open Goptions
 
@@ -62,20 +62,35 @@ type form=
   | Conjunct of form * form
   | Disjunct of form * form
 
-type tag=int
-
-let decomp_form=function
-    Atom i -> Some (i,[])
-  | Arrow (f1,f2) -> Some (-1,[f1;f2])
-  | Bot -> Some (-2,[])
-  | Conjunct (f1,f2) -> Some (-3,[f1;f2])
-  | Disjunct (f1,f2) -> Some (-4,[f1;f2])
-
-module Fmap=Map.Make(struct type t=form let compare=compare end)
+module FOrd = struct
+  type t = form
+  let rec compare x y =
+    match x, y with
+    | Bot, Bot -> 0
+    | Bot, _ -> -1
+    | Atom _, Bot -> 1
+    | Atom a1, Atom a2 -> Int.compare a1 a2
+    | Atom _, _ -> -1
+    | Arrow _, (Bot | Atom _) -> 1
+    | Arrow (f1, g1), Arrow (f2, g2) ->
+        let cmp = compare f1 f2 in
+        if cmp = 0 then compare g1 g2 else cmp
+    | Arrow _, _ -> -1
+    | Conjunct _, (Bot | Atom _ | Arrow _) -> 1
+    | Conjunct (f1, g1), Conjunct (f2, g2) ->
+        let cmp = compare f1 f2 in
+        if cmp = 0 then compare g1 g2 else cmp
+    | Conjunct _, _ -> -1
+    | Disjunct _, (Bot | Atom _ | Arrow _ | Conjunct _) -> 1
+    | Disjunct (f1, g1), Disjunct (f2, g2) ->
+        let cmp = compare f1 f2 in
+        if cmp = 0 then compare g1 g2 else cmp
+end
+module Fmap = Map.Make(FOrd)
 
 type sequent =
-    {rev_hyps: form Intmap.t;
-     norev_hyps: form Intmap.t;
+    {rev_hyps: form Int.Map.t;
+     norev_hyps: form Int.Map.t;
      size:int;
      left:int Fmap.t;
      right:(int*form) list Fmap.t;
@@ -131,21 +146,21 @@ 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 "add_step: wrong arity"
+    | _,_ -> anomaly ~label:"add_step" (Pp.str "wrong arity")
 
 type 'a with_deps =
     {dep_it:'a;
      dep_goal:bool;
-     dep_hyps:Intset.t}
+     dep_hyps:Int.Set.t}
 
 type slice=
     {proofs_done:proof list;
      proofs_todo:sequent with_deps list;
      step:rule;
      needs_goal:bool;
-     needs_hyps:Intset.t;
+     needs_hyps:Int.Set.t;
      changes_goal:bool;
-     creates_hyps:Intset.t}
+     creates_hyps:Int.Set.t}
 
 type state =
     Complete of proof
@@ -153,7 +168,7 @@ type state =
 
 let project = function
     Complete prf -> prf
-  | Incomplete (_,_) -> anomaly "not a successful state"
+  | Incomplete (_,_) -> anomaly (Pp.str "not a successful state")
 
 let pop n prf =
   let nprf=
@@ -168,27 +183,27 @@ let rec fill stack proof =
     | slice::super ->
 	if
 	  !pruning &&
-	  slice.proofs_done=[] &&
+	  List.is_empty slice.proofs_done &&
 	  not (slice.changes_goal && proof.dep_goal) &&
-	  not (Intset.exists
-		 (fun i -> Intset.mem i proof.dep_hyps)
+	  not (Int.Set.exists
+		 (fun i -> Int.Set.mem i proof.dep_hyps)
 		 slice.creates_hyps)
 	then
 	  begin
 	    s_info.pruned_steps<-s_info.pruned_steps+1;
 	    s_info.pruned_branches<- s_info.pruned_branches +
 	    List.length slice.proofs_todo;
-	    let created_here=Intset.cardinal slice.creates_hyps in
+	    let created_here=Int.Set.cardinal slice.creates_hyps in
 	      s_info.pruned_hyps<-s_info.pruned_hyps+
 	      List.fold_left
-		(fun sum dseq -> sum + Intset.cardinal dseq.dep_hyps)
+		(fun sum dseq -> sum + Int.Set.cardinal dseq.dep_hyps)
 		created_here slice.proofs_todo;
-	    fill super (pop (Intset.cardinal slice.creates_hyps) proof)
+	    fill super (pop (Int.Set.cardinal slice.creates_hyps) proof)
 	  end
 	else
 	  let dep_hyps=
-	    Intset.union slice.needs_hyps
-	      (Intset.diff proof.dep_hyps slice.creates_hyps) in
+	    Int.Set.union slice.needs_hyps
+	      (Int.Set.diff proof.dep_hyps slice.creates_hyps) in
 	  let dep_goal=
 	    slice.needs_goal ||
 	    ((not slice.changes_goal) && proof.dep_goal) in
@@ -235,7 +250,7 @@ let append stack (step,subgoals) =
 let embed seq=
   {dep_it=seq;
    dep_goal=false;
-   dep_hyps=Intset.empty}
+   dep_hyps=Int.Set.empty}
 
 let change_goal seq gl=
     {seq with
@@ -270,7 +285,7 @@ let add_hyp seqwd f=
 	     cnx=cnx}
       | Conjunct (_,_) | Disjunct (_,_) ->
 	  {seq with
-	     rev_hyps=Intmap.add num f seq.rev_hyps;
+	     rev_hyps=Int.Map.add num f seq.rev_hyps;
 	     size=num;
 	     left=left;
 	     right=right;
@@ -285,14 +300,14 @@ let add_hyp seqwd f=
 	    match f1 with
 		Conjunct (_,_) | Disjunct (_,_) ->
 		  {seq with
-		     rev_hyps=Intmap.add num f seq.rev_hyps;
+		     rev_hyps=Int.Map.add num f seq.rev_hyps;
 		     size=num;
 		     left=left;
 		     right=nright;
 		     cnx=ncnx}
 	      | Arrow(_,_) ->
 		  {seq with
-		     norev_hyps=Intmap.add num f seq.norev_hyps;
+		     norev_hyps=Int.Map.add num f seq.norev_hyps;
 		     size=num;
 		     left=left;
 		     right=nright;
@@ -305,13 +320,13 @@ let add_hyp seqwd f=
 		     cnx=ncnx} in
     {seqwd with
        dep_it=nseq;
-       dep_hyps=Intset.add num seqwd.dep_hyps}
+       dep_hyps=Int.Set.add num seqwd.dep_hyps}
 
 exception Here_is of (int*form)
 
 let choose m=
   try
-    Intmap.iter (fun i f -> raise (Here_is (i,f))) m;
+    Int.Map.iter (fun i f -> raise (Here_is (i,f))) m;
     raise Not_found
   with
       Here_is (i,f) -> (i,f)
@@ -322,11 +337,11 @@ let search_or seq=
       Disjunct (f1,f2) ->
 	[{dep_it = SI_Or_l;
 	  dep_goal = true;
-	  dep_hyps = Intset.empty},
+	  dep_hyps = Int.Set.empty},
 	 [change_goal (embed seq) f1];
 	 {dep_it = SI_Or_r;
 	  dep_goal = true;
-	  dep_hyps = Intset.empty},
+	  dep_hyps = Int.Set.empty},
 	 [change_goal (embed seq) f2]]
     | _ -> []
 
@@ -336,19 +351,19 @@ let search_norev seq=
     match f with
 	Arrow (Arrow (f1,f2),f3) ->
 	  let nseq =
-	    {seq with norev_hyps=Intmap.remove i seq.norev_hyps} in
+	    {seq with norev_hyps=Int.Map.remove i seq.norev_hyps} in
 	    goals:=
 	      ({dep_it=SD_Arrow(i);
 		dep_goal=false;
-		dep_hyps=Intset.singleton i},
+		dep_hyps=Int.Set.singleton i},
 	       [add_hyp
 		  (add_hyp
 		     (change_goal (embed nseq) f2)
 		     (Arrow(f2,f3)))
 		  f1;
 		add_hyp (embed nseq) f3]):: !goals
-      | _ -> anomaly "search_no_rev: can't happen" in
-    Intmap.iter add_one seq.norev_hyps;
+      | _ -> anomaly ~label:"search_no_rev" (Pp.str "can't happen") in
+    Int.Map.iter add_one seq.norev_hyps;
     List.rev !goals
 
 let search_in_rev_hyps seq=
@@ -357,8 +372,8 @@ let search_in_rev_hyps seq=
     let make_step step=
       {dep_it=step;
        dep_goal=false;
-       dep_hyps=Intset.singleton i} in
-    let nseq={seq with rev_hyps=Intmap.remove i seq.rev_hyps} in
+       dep_hyps=Int.Set.singleton i} in
+    let nseq={seq with rev_hyps=Int.Map.remove i seq.rev_hyps} in
       match f with
 	  Conjunct (f1,f2) ->
 	    [make_step (SE_And(i)),
@@ -372,7 +387,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 "search_in_rev_hyps: can't happen"
+	| _ -> anomaly ~label:"search_in_rev_hyps" (Pp.str "can't happen")
   with
       Not_found -> search_norev seq
 
@@ -383,27 +398,27 @@ let search_rev seq=
 	  match f1 with
 	      Conjunct (_,_) | Disjunct (_,_) ->
 		{seq with cnx=next;
-		   rev_hyps=Intmap.remove j seq.rev_hyps}
+		   rev_hyps=Int.Map.remove j seq.rev_hyps}
 	    | Arrow (_,_) ->
 		{seq with cnx=next;
-		   norev_hyps=Intmap.remove j seq.norev_hyps}
+		   norev_hyps=Int.Map.remove j seq.norev_hyps}
 	    | _ ->
 		{seq with cnx=next} in
 	  [{dep_it=SE_Arrow(i,j);
 	    dep_goal=false;
-	    dep_hyps=Intset.add i (Intset.singleton j)},
+	    dep_hyps=Int.Set.add i (Int.Set.singleton j)},
 	   [add_hyp (embed nseq) f2]]
     | [] ->
 	match seq.gl with
 	    Arrow (f1,f2) ->
 	      [{dep_it=SI_Arrow;
 		dep_goal=true;
-		dep_hyps=Intset.empty},
+		dep_hyps=Int.Set.empty},
 	       [add_hyp (change_goal (embed seq) f2) f1]]
 	  | Conjunct (f1,f2) ->
 	      [{dep_it=SI_And;
 		dep_goal=true;
-		dep_hyps=Intset.empty},[change_goal (embed seq) f1;
+		dep_hyps=Int.Set.empty},[change_goal (embed seq) f1;
 					change_goal (embed seq) f2]]
 	  | _ -> search_in_rev_hyps seq
 
@@ -412,18 +427,18 @@ let search_all seq=
       Some i ->
 	[{dep_it=SE_False (i);
 	  dep_goal=false;
-	  dep_hyps=Intset.singleton i},[]]
+	  dep_hyps=Int.Set.singleton i},[]]
     | None ->
 	try
 	  let ax = Fmap.find seq.gl seq.left in
 	    [{dep_it=SAx (ax);
 	      dep_goal=true;
-	      dep_hyps=Intset.singleton ax},[]]
+	      dep_hyps=Int.Set.singleton ax},[]]
 	with Not_found -> search_rev seq
 
 let bare_sequent = embed
-		     {rev_hyps=Intmap.empty;
-		      norev_hyps=Intmap.empty;
+		     {rev_hyps=Int.Map.empty;
+		      norev_hyps=Int.Map.empty;
 		      size=0;
 		      left=Fmap.empty;
 		      right=Fmap.empty;
@@ -442,7 +457,7 @@ let success= function
 
 let branching = function
     Incomplete (seq,stack) ->
-      check_for_interrupt ();
+      Control.check_for_interrupt ();
       let successors = search_all seq in
       let _ =
 	match successors with
@@ -450,7 +465,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 "already succeeded"
+  | Complete prf -> anomaly (Pp.str "already succeeded")
 
 open Pp
 
@@ -471,11 +486,11 @@ and pp_atom= function
   | Atom n -> int n
   | f -> str "(" ++ hv 2 (pp_form f) ++ str ")"
 
-let pr_form f = msg (pp_form f)
+let pr_form f = pp_form f
 
 let pp_intmap map =
   let pp=ref (str "") in
-   Intmap.iter (fun i obj -> pp:= (!pp ++
+   Int.Map.iter (fun i obj -> pp:= (!pp ++
 		pp_form obj ++ cut ())) map;
     str "{ " ++ v 0 (!pp) ++ str " }"
 
@@ -532,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
-    msgnl
+    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 1aaafbe6..86a2fb66 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-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -40,7 +40,7 @@ val success: state -> bool
 
 val pp: state -> Pp.std_ppcmds
 
-val pr_form : form -> unit
+val pr_form : form -> Pp.std_ppcmds
 
 val reset_info : unit -> unit
 
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 7dedb44e..4ffc1f33 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-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,10 +8,9 @@
 
 module Search = Explore.Make(Proof_search)
 
+open Errors
 open Util
 open Term
-open Names
-open Evd
 open Tacmach
 open Proof_search
 
@@ -28,13 +27,6 @@ let li_False = lazy (destInd (logic_constant "False"))
 let li_and = lazy (destInd (logic_constant "and"))
 let li_or =  lazy (destInd (logic_constant "or"))
 
-let data_constant =
-  Coqlib.gen_constant "refl_tauto" ["Init";"Datatypes"]
-
-let l_true_equals_true =
-  lazy (mkApp(logic_constant "eq_refl",
-        [|data_constant "bool";data_constant "true"|]))
-
 let pos_constant =
   Coqlib.gen_constant "refl_tauto" ["Numbers";"BinNums"]
 
@@ -103,7 +95,7 @@ let rec make_form atom_env gls term =
 	Prod(_,a,b) ->
 	  if not (Termops.dependent (mkRel 1) b) &&
 	    Retyping.get_sort_family_of
-	    (pf_env gls) (Tacmach.project gls) a = InProp
+	    (pf_env gls) (Tacmach.project gls) a == InProp
 	  then
 	    let fa=make_form atom_env gls a in
 	    let fb=make_form atom_env gls b in
@@ -112,25 +104,25 @@ let rec make_form atom_env gls term =
 	    make_atom atom_env (normalize term)
       | Cast(a,_,_) ->
 	  make_form atom_env gls a
-      | Ind ind ->
-	  if ind = Lazy.force li_False then
+      | Ind (ind, _) ->
+	  if Names.eq_ind ind (fst (Lazy.force li_False)) then
 	    Bot
 	  else
 	    make_atom atom_env (normalize term)
-      | App(hd,argv) when Array.length argv = 2 ->
+      | App(hd,argv) when Int.equal (Array.length argv) 2 ->
 	  begin
 	    try
-	      let ind = destInd hd in
-		if ind = Lazy.force li_and then
+	      let ind, _ = destInd hd in
+		if Names.eq_ind ind (fst (Lazy.force li_and)) then
 		  let fa=make_form atom_env gls argv.(0) in
 		  let fb=make_form atom_env gls argv.(1) in
 		    Conjunct (fa,fb)
-		else if ind = Lazy.force li_or then
+		else if Names.eq_ind ind (fst (Lazy.force li_or)) then
 		  let fa=make_form atom_env gls argv.(0) in
 		  let fb=make_form atom_env gls argv.(1) in
 		    Disjunct (fa,fb)
 		else make_atom atom_env (normalize term)
-	    with Invalid_argument _ -> make_atom atom_env (normalize term)
+	    with DestKO -> make_atom atom_env (normalize term)
 	  end
       | _ -> make_atom atom_env (normalize term)
 
@@ -143,7 +135,7 @@ let rec make_hyps atom_env gls lenv = function
 	make_hyps atom_env gls (typ::lenv) rest in
 	if List.exists (Termops.dependent (mkVar id)) lenv ||
 	  (Retyping.get_sort_family_of
-	     (pf_env gls) (Tacmach.project gls) typ <> InProp)
+	     (pf_env gls) (Tacmach.project gls) typ != InProp)
 	then
 	  hrec
 	else
@@ -151,7 +143,7 @@ let rec make_hyps atom_env gls lenv = function
 
 let rec build_pos n =
   if n<=1 then force node_count l_xH
-  else if n land 1 = 0 then
+  else if Int.equal (n land 1) 0 then
     mkApp (force node_count l_xO,[|build_pos (n asr 1)|])
   else
     mkApp (force node_count l_xI,[|build_pos (n asr 1)|])
@@ -269,22 +261,21 @@ let rtauto_tac gls=
   let gl=pf_concl gls in
   let _=
     if Retyping.get_sort_family_of
-      (pf_env gls) (Tacmach.project gls) gl <> InProp
+      (pf_env gls) (Tacmach.project gls) gl != InProp
     then errorlabstrm "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=
     List.fold_left (fun gl (_,f)-> Arrow (f,gl)) glf hyps in
-  let search_fun =
-    if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 then
-      Search.debug_depth_first
-    else
-      Search.depth_first in
+  let search_fun = match Tacinterp.get_debug() with
+  | Tactic_debug.DebugOn 0 -> Search.debug_depth_first
+  | _ -> Search.depth_first
+  in
   let _ =
     begin
       reset_info ();
       if !verbose then
-	msgnl (str "Starting proof-search ...");
+	msg_info (str "Starting proof-search ...");
     end in
   let search_start_time = System.get_time () in
   let prf =
@@ -294,10 +285,10 @@ let rtauto_tac gls=
   let search_end_time = System.get_time () in
   let _ = if !verbose then
     begin
-      msgnl (str "Proof tree found in " ++
+      msg_info (str "Proof tree found in " ++
 	     System.fmt_time_difference search_start_time search_end_time);
       pp_info ();
-      msgnl (str "Building proof term ... ")
+      msg_info (str "Building proof term ... ")
     end in
   let build_start_time=System.get_time () in
   let _ = step_count := 0; node_count := 0 in
@@ -306,11 +297,11 @@ let rtauto_tac gls=
 		      build_form formula;
 		      build_proof [] 0 prf|]) in
   let term=
-    Term.applist (main,List.rev_map (fun (id,_) -> mkVar id) hyps) in
+    applist (main,List.rev_map (fun (id,_) -> mkVar id) hyps) in
   let build_end_time=System.get_time () in
   let _ = if !verbose then
     begin
-      msgnl (str "Proof term built in " ++
+      msg_info (str "Proof term built in " ++
 	     System.fmt_time_difference build_start_time build_end_time ++
 	     fnl () ++
 	     str "Proof size : " ++ int !step_count ++
@@ -322,14 +313,14 @@ let rtauto_tac gls=
   let tac_start_time = System.get_time () in
   let result=
     if !check then
-      Tactics.exact_check term gls
+      Proofview.V82.of_tactic (Tactics.exact_check term) gls
     else
       Tactics.exact_no_check term gls in
   let tac_end_time = System.get_time () in
   let _ =
-    if !check then msgnl (str "Proof term type-checking is on");
+    if !check then msg_info (str "Proof term type-checking is on");
     if !verbose then
-      msgnl (str "Internal tactic executed in " ++
+      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 9f7db593..45fb50dc 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-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \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.identifier * Term.types option * Term.types) list ->
-    (Names.identifier * Proof_search.form) list
+    (Names.Id.t * Term.types option * Term.types) list ->
+    (Names.Id.t * Proof_search.form) list
 
 val rtauto_tac : Proof_type.tactic