Imported Upstream version 8.4~betaupstream/8.4_beta

7 files changed, 89 insertions, 217 deletions

diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index 39c29a3d..77f8f834 100644
--- a/plugins/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
@@ -1,154 +1,32 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Bintree.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 Require Export List.
 Require Export BinPos.
-
-Unset Boxed Definitions.
+Require Arith.EqNat.
 
 Open Scope positive_scope.
 
 Ltac clean := try (simpl; congruence).
-Ltac caseq t := generalize (refl_equal t); pattern t at -1; case t.
-
-Functional Scheme Pcompare_ind := Induction for Pcompare Sort Prop.
-
-Lemma Gt_Eq_Gt : forall p q cmp,
-       (p ?= q) Eq = Gt -> (p ?= q) cmp = Gt.
-apply (Pcompare_ind (fun p q cmp _ => (p ?= q) Eq = Gt -> (p ?= q) cmp = Gt));
-simpl;auto;congruence.
-Qed.
-
-Lemma Gt_Lt_Gt : forall p q cmp,
-       (p ?= q) Lt = Gt -> (p ?= q) cmp = Gt.
-apply (Pcompare_ind (fun p q cmp _ => (p ?= q) Lt = Gt -> (p ?= q) cmp = Gt));
-simpl;auto;congruence.
-Qed.
-
-Lemma Gt_Psucc_Eq: forall p q,
-  (p ?= Psucc q) Gt = Gt -> (p ?= q) Eq = Gt.
-intros p q;generalize p;clear p;induction q;destruct p;simpl;auto;try congruence.
-intro;apply Gt_Eq_Gt;auto.
-apply Gt_Lt_Gt.
-Qed.
-
-Lemma Eq_Psucc_Gt: forall p q,
-  (p ?= Psucc q) Eq = Eq -> (p ?= q) Eq = Gt.
-intros p q;generalize p;clear p;induction q;destruct p;simpl;auto;try congruence.
-intro H;elim (Pcompare_not_Eq p (Psucc q));tauto.
-intro H;apply Gt_Eq_Gt;auto.
-intro H;rewrite Pcompare_Eq_eq with p q;auto.
-generalize q;clear q IHq p H;induction q;simpl;auto.
-intro H;elim (Pcompare_not_Eq p q);tauto.
-Qed.
-
-Lemma Gt_Psucc_Gt : forall n p cmp cmp0,
- (n?=p) cmp = Gt -> (Psucc n?=p) cmp0 = Gt.
-induction n;intros [ | p | p];simpl;try congruence.
-intros; apply IHn with cmp;trivial.
-intros; apply IHn with Gt;trivial.
-intros;apply Gt_Lt_Gt;trivial.
-intros [ | | ] _ H.
-apply Gt_Eq_Gt;trivial.
-apply Gt_Lt_Gt;trivial.
-trivial.
-Qed.
 
 Lemma Gt_Psucc: forall p q,
-       (p ?= Psucc q) Eq = Gt -> (p ?= q) Eq = Gt.
-intros p q;generalize p;clear p;induction q;destruct p;simpl;auto;try congruence.
-apply Gt_Psucc_Eq.
-intro;apply Gt_Eq_Gt;apply IHq;auto.
-apply Gt_Eq_Gt.
-apply Gt_Lt_Gt.
+       (p ?= Psucc q) = Gt -> (p ?= q) = Gt.
+Proof.
+intros. rewrite <- Pos.compare_succ_succ.
+now apply Pos.lt_gt, Pos.lt_lt_succ, Pos.gt_lt.
 Qed.
 
 Lemma Psucc_Gt : forall p,
-       (Psucc p ?= p) Eq = Gt.
-induction p;simpl.
-apply Gt_Eq_Gt;auto.
-generalize p;clear p IHp.
-induction p;simpl;auto.
-reflexivity.
+       (Psucc p ?= p) = Gt.
+Proof.
+intros. apply Pos.lt_gt, Pos.lt_succ_diag_r.
 Qed.
 
-Fixpoint pos_eq (m n:positive) {struct m} :bool :=
-match m, n with
-  xI mm, xI nn => pos_eq mm nn
-| xO mm, xO nn => pos_eq mm nn
-| xH, xH => true
-| _, _ => false
-end.
-
-Theorem pos_eq_refl : forall m n, pos_eq m n = true -> m = n.
-induction m;simpl;intro n;destruct n;congruence ||
-(intro e;apply f_equal with positive;auto).
-Defined.
-
-Theorem refl_pos_eq : forall m, pos_eq m m = true.
-induction m;simpl;auto.
-Qed.
-
-Definition pos_eq_dec : forall (m n:positive), {m=n}+{m<>n} .
-fix 1;intros [mm|mm|] [nn|nn|];try (right;congruence).
-case (pos_eq_dec mm nn).
-intro e;left;apply (f_equal xI e).
-intro ne;right;congruence.
-case (pos_eq_dec mm nn).
-intro e;left;apply (f_equal xO e).
-intro ne;right;congruence.
-left;reflexivity.
-Defined.
-
-Theorem pos_eq_dec_refl : forall m, pos_eq_dec m m = left _ (refl_equal m).
-fix 1;intros [mm|mm|].
-simpl; rewrite  pos_eq_dec_refl; reflexivity.
-simpl; rewrite  pos_eq_dec_refl; reflexivity.
-reflexivity.
-Qed.
-
-Theorem pos_eq_dec_ex : forall m n,
- pos_eq m n =true -> exists h:m=n,
- pos_eq_dec m n = left _ h.
-fix 1;intros [mm|mm|] [nn|nn|];try (simpl;congruence).
-simpl;intro e.
-elim (pos_eq_dec_ex _ _ e).
-intros x ex; rewrite ex.
-exists (f_equal xI x).
-reflexivity.
-simpl;intro e.
-elim (pos_eq_dec_ex _ _ e).
-intros x ex; rewrite ex.
-exists (f_equal xO x).
-reflexivity.
-simpl.
-exists (refl_equal xH).
-reflexivity.
-Qed.
-
-Fixpoint nat_eq (m n:nat) {struct m}: bool:=
-match m, n with
-O,O => true
-| S mm,S nn => nat_eq mm nn
-| _,_ => false
-end.
-
-Theorem nat_eq_refl : forall m n, nat_eq m n = true -> m = n.
-induction m;simpl;intro n;destruct n;congruence ||
-(intro e;apply f_equal with nat;auto).
-Defined.
-
-Theorem refl_nat_eq : forall n, nat_eq n n = true.
-induction n;simpl;trivial.
-Defined.
-
 Fixpoint Lget (A:Set) (n:nat) (l:list A) {struct l}:option A :=
 match l with nil => None
 | x::q =>
@@ -156,21 +34,21 @@ match n with O => Some x
 | S m => Lget A m q
 end end .
 
-Implicit Arguments Lget [A].
+Arguments Lget [A] n l.
 
 Lemma map_app : forall (A B:Set) (f:A -> B) l m,
 List.map  f (l ++ m) = List.map  f  l ++ List.map  f  m.
 induction l.
 reflexivity.
 simpl.
-intro m ; apply f_equal with (list B);apply IHl.
+intro m ; apply f_equal;apply IHl.
 Qed.
 
 Lemma length_map : forall (A B:Set) (f:A -> B) l,
 length (List.map  f l) = length l.
 induction l.
 reflexivity.
-simpl; apply f_equal with nat;apply IHl.
+simpl; apply f_equal;apply IHl.
 Qed.
 
 Lemma Lget_map : forall (A B:Set) (f:A -> B) i l,
@@ -182,7 +60,8 @@ simpl;auto.
 Qed.
 
 Lemma Lget_app : forall (A:Set) (a:A) l i,
-Lget i (l ++ a :: nil) = if nat_eq i (length l) then Some a else Lget i l.
+Lget i (l ++ a :: nil) = if Arith.EqNat.beq_nat i (length l) then Some a else Lget i l.
+Proof.
 induction l;simpl Lget;simpl length.
 intros [ | i];simpl;reflexivity.
 intros [ | i];simpl.
@@ -278,17 +157,20 @@ Qed.
 
 Theorem Tget_Tadd: forall i j a T,
        Tget i (Tadd j a T) =
-       match (i ?= j) Eq with
+       match (i ?= j) with
          Eq => PSome a
        | Lt => Tget i T
        | Gt => Tget i T
        end.
+Proof.
 intros i j.
-caseq ((i ?= j) Eq).
-intro H;rewrite (Pcompare_Eq_eq _ _ H);intros a;clear i H.
+case_eq (i ?= j).
+intro H;rewrite (Pos.compare_eq _ _ H);intros a;clear i H.
 induction j;destruct T;simpl;try (apply IHj);congruence.
+unfold Pos.compare.
 generalize i;clear i;induction j;destruct T;simpl in H|-*;
 destruct i;simpl;try rewrite (IHj _ H);try (destruct i;simpl;congruence);reflexivity|| congruence.
+unfold Pos.compare.
 generalize i;clear i;induction j;destruct T;simpl in H|-*;
 destruct i;simpl;try rewrite (IHj _ H);try (destruct i;simpl;congruence);reflexivity|| congruence.
 Qed.
@@ -312,7 +194,8 @@ Inductive Full : Store -> Type:=
   | F_push : forall a S, Full S -> Full (push a S).
 
 Theorem get_Full_Gt : forall S, Full S ->
-       forall i, (i ?= index S) Eq = Gt -> get i S = PNone.
+       forall i, (i ?= index S) = Gt -> get i S = PNone.
+Proof.
 intros S W;induction W.
 unfold empty,index,get,contents;intros;apply Tget_Tempty.
 unfold index,get,push;simpl contents.
@@ -339,16 +222,17 @@ Qed.
 Theorem get_push_Full :
   forall i a S, Full S ->
   get i (push a S) =
-  match (i ?= index S) Eq with
+  match (i ?= index S) with
     Eq => PSome a
   | Lt => get i S
   | Gt => PNone
 end.
+Proof.
 intros i a S F.
-caseq ((i ?= index S) Eq).
-intro e;rewrite (Pcompare_Eq_eq _ _ e).
+case_eq (i ?= index S).
+intro e;rewrite (Pos.compare_eq _ _ e).
 destruct S;unfold get,push,index;simpl contents;rewrite Tget_Tadd.
-rewrite Pcompare_refl;reflexivity.
+rewrite Pos.compare_refl;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.
@@ -361,8 +245,9 @@ Qed.
 Lemma Full_push_compat : forall i a S, Full S ->
 forall x, get i S = PSome x ->
  get i (push a S) = PSome x.
+Proof.
 intros i a S F x H.
-caseq ((i ?= index S) Eq);intro test.
+case_eq (i ?= index S);intro test.
 rewrite (Pcompare_Eq_eq _ _ test) in H.
 rewrite (get_Full_Eq _ F) in H;congruence.
 rewrite <- H.
@@ -395,7 +280,7 @@ get i S = PSome x -> In x S F.
 induction F.
 intro i;rewrite get_empty; congruence.
 intro i;rewrite get_push_Full;trivial.
-caseq ((i ?= index S) Eq);simpl.
+case_eq (i ?= index S);simpl.
 left;congruence.
 right;eauto.
 congruence.
@@ -403,34 +288,34 @@ Qed.
 
 End Store.
 
-Implicit Arguments PNone [A].
-Implicit Arguments PSome [A].
+Arguments PNone [A].
+Arguments PSome [A] _.
 
-Implicit Arguments Tempty [A].
-Implicit Arguments Branch0 [A].
-Implicit Arguments Branch1 [A].
+Arguments Tempty [A].
+Arguments Branch0 [A] _ _.
+Arguments Branch1 [A] _ _ _.
 
-Implicit Arguments Tget [A].
-Implicit Arguments Tadd [A].
+Arguments Tget [A] p T.
+Arguments Tadd [A] p a T.
 
-Implicit Arguments Tget_Tempty [A].
-Implicit Arguments Tget_Tadd [A].
+Arguments Tget_Tempty [A] p.
+Arguments Tget_Tadd [A] i j a T.
 
-Implicit Arguments mkStore [A].
-Implicit Arguments index [A].
-Implicit Arguments contents [A].
+Arguments mkStore [A] index contents.
+Arguments index [A] s.
+Arguments contents [A] s.
 
-Implicit Arguments empty [A].
-Implicit Arguments get [A].
-Implicit Arguments push [A].
+Arguments empty [A].
+Arguments get [A] i S.
+Arguments push [A] a S.
 
-Implicit Arguments get_empty [A].
-Implicit Arguments get_push_Full [A].
+Arguments get_empty [A] i.
+Arguments get_push_Full [A] i a S _.
 
-Implicit Arguments Full [A].
-Implicit Arguments F_empty [A].
-Implicit Arguments F_push [A].
-Implicit Arguments In [A].
+Arguments Full [A] _.
+Arguments F_empty [A].
+Arguments F_push [A] a S _.
+Arguments In [A] x S F.
 
 Section Map.
 
@@ -482,8 +367,8 @@ Defined.
 
 End Map.
 
-Implicit Arguments Tmap [A B].
-Implicit Arguments map [A B].
-Implicit Arguments Full_map [A B f].
+Arguments Tmap [A B] f T.
+Arguments map [A B] f S.
+Arguments Full_map [A B f] S _.
 
 Notation "hyps \ A" := (push A hyps) (at level 72,left associativity).
diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v
index 3817f98c..9cae7a44 100644
--- a/plugins/rtauto/Rtauto.v
+++ b/plugins/rtauto/Rtauto.v
@@ -1,22 +1,18 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Rtauto.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 
 Require Export List.
 Require Export Bintree.
 Require Import Bool.
-Unset Boxed Definitions.
 
 Declare ML Module "rtauto_plugin".
 
-Ltac caseq t := generalize (refl_equal t); pattern t at -1; case t.
 Ltac clean:=try (simpl;congruence).
 
 Inductive form:Set:=
@@ -43,7 +39,7 @@ end.
 
 Theorem pos_eq_refl : forall m n, pos_eq m n = true -> m = n.
 induction m;simpl;destruct n;congruence ||
-(intro e;apply f_equal with positive;auto).
+(intro e;apply f_equal;auto).
 Qed.
 
 Fixpoint form_eq (p q:form) {struct p} :bool :=
@@ -69,15 +65,15 @@ end.
 Theorem form_eq_refl: forall p q, form_eq p q = true -> p = q.
 induction p;destruct q;simpl;clean.
 intro h;generalize (pos_eq_refl _ _ h);congruence.
-caseq (form_eq p1 q1);clean.
+case_eq (form_eq p1 q1);clean.
 intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence.
-caseq (form_eq p1 q1);clean.
+case_eq (form_eq p1 q1);clean.
 intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence.
-caseq (form_eq p1 q1);clean.
+case_eq (form_eq p1 q1);clean.
 intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence.
 Qed.
 
-Implicit Arguments form_eq_refl [p q].
+Arguments form_eq_refl [p q] _.
 
 Section with_env.
 
@@ -165,7 +161,7 @@ intros hyps F p g e; apply project_In.
 apply get_In with p;assumption.
 Qed.
 
-Implicit Arguments project [hyps p g].
+Arguments project [hyps] F [p g] _.
 
 Inductive proof:Set :=
   Ax : positive -> proof
@@ -263,7 +259,7 @@ induction p;intros hyps F gl.
 
 (* cas Axiom *)
 Focus 1.
-simpl;caseq (get p hyps);clean.
+simpl;case_eq (get p hyps);clean.
 intros f nth_f e;rewrite <- (form_eq_refl e).
 apply project with p;trivial.
 
@@ -276,10 +272,10 @@ apply IHp;try constructor;trivial.
 
 (* Cas Arrow_Elim *)
 Focus 1.
-simpl check_proof;caseq (get p hyps);clean.
-intros f ef;caseq (get p0 hyps);clean.
+simpl check_proof;case_eq (get p hyps);clean.
+intros f ef;case_eq (get p0 hyps);clean.
 intros f0 ef0;destruct f0;clean.
-caseq (form_eq f f0_1);clean.
+case_eq (form_eq f f0_1);clean.
 simpl;intros e check_p1.
 generalize  (project  F ef) (project  F ef0)
 (IHp (hyps \ f0_2) (F_push f0_2 hyps F) gl check_p1);
@@ -291,10 +287,10 @@ auto.
 
 (* cas Arrow_Destruct *)
 Focus 1.
-simpl;caseq (get p1 hyps);clean.
+simpl;case_eq (get p1 hyps);clean.
 intros f ef;destruct f;clean.
 destruct f1;clean.
-caseq (check_proof (hyps \ f1_2 =>> f2 \ f1_1) f1_2 p2);clean.
+case_eq (check_proof (hyps \ f1_2 =>> f2 \ f1_1) f1_2 p2);clean.
 intros check_p1 check_p2.
 generalize (project F ef)
 (IHp1 (hyps \ f1_2 =>> f2 \ f1_1)
@@ -305,7 +301,7 @@ simpl;apply compose3;auto.
 
 (* Cas False_Elim *)
 Focus 1.
-simpl;caseq (get p hyps);clean.
+simpl;case_eq (get p hyps);clean.
 intros f ef;destruct f;clean.
 intros _; generalize (project F ef).
 apply compose1;apply False_ind.
@@ -313,13 +309,13 @@ apply compose1;apply False_ind.
 (* Cas And_Intro *)
 Focus 1.
 simpl;destruct gl;clean.
-caseq (check_proof hyps gl1 p1);clean.
+case_eq (check_proof hyps gl1 p1);clean.
 intros Hp1 Hp2;generalize (IHp1 hyps F gl1 Hp1) (IHp2 hyps F gl2 Hp2).
 apply compose2 ;simpl;auto.
 
 (* cas And_Elim *)
 Focus 1.
-simpl;caseq (get p hyps);clean.
+simpl;case_eq (get p hyps);clean.
 intros f ef;destruct f;clean.
 intro check_p;generalize  (project F ef)
 (IHp (hyps \ f1 \ f2) (F_push f2 (hyps \ f1) (F_push f1 hyps F)) gl check_p).
@@ -327,7 +323,7 @@ simpl;apply compose2;intros [h1 h2];auto.
 
 (* cas And_Destruct *)
 Focus 1.
-simpl;caseq (get p hyps);clean.
+simpl;case_eq (get p hyps);clean.
 intros f ef;destruct f;clean.
 destruct f1;clean.
 intro H;generalize  (project F ef)
@@ -349,9 +345,9 @@ apply compose1;simpl;auto.
 
 (* cas Or_elim *)
 Focus 1.
-simpl;caseq (get p1 hyps);clean.
+simpl;case_eq (get p1 hyps);clean.
 intros f ef;destruct f;clean.
-caseq (check_proof (hyps \ f1) gl p2);clean.
+case_eq (check_proof (hyps \ f1) gl p2);clean.
 intros check_p1 check_p2;generalize (project F ef)
 (IHp1 (hyps \ f1) (F_push f1 hyps F) gl check_p1)
 (IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2);
@@ -359,7 +355,7 @@ simpl;apply compose3;simpl;intro h;destruct h;auto.
 
 (* cas Or_Destruct *)
 Focus 1.
-simpl;caseq (get p hyps);clean.
+simpl;case_eq (get p hyps);clean.
 intros f ef;destruct f;clean.
 destruct f1;clean.
 intro check_p0;generalize (project F ef)
@@ -370,7 +366,7 @@ apply compose2;auto.
 
 (* cas Cut *)
 Focus 1.
-simpl;caseq (check_proof hyps f p1);clean.
+simpl;case_eq (check_proof hyps f p1);clean.
 intros check_p1 check_p2;
 generalize (IHp1 hyps F f check_p1)
 (IHp2 (hyps\f) (F_push f hyps F) gl check_p2);
@@ -378,7 +374,7 @@ simpl; apply compose2;auto.
 Qed.
 
 Theorem Reflect: forall gl prf, if check_proof empty gl prf then [[gl]] else True.
-intros gl prf;caseq (check_proof empty gl prf);intro check_prf.
+intros gl prf;case_eq (check_proof empty gl prf);intro check_prf.
 change (interp_ctx empty F_empty [[gl]]) ;
 apply interp_proof with prf;assumption.
 trivial.
diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4
index 552f23f6..8d103d1b 100644
--- a/plugins/rtauto/g_rtauto.ml4
+++ b/plugins/rtauto/g_rtauto.ml4
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: g_rtauto.ml4 14641 2011-11-06 11:59:10Z herbelin $*)
-
 (*i camlp4deps: "parsing/grammar.cma"  i*)
 
 TACTIC EXTEND rtauto
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 500138cf..d773b153 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: proof_search.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Term
 open Util
 open Goptions
@@ -49,6 +47,7 @@ let pruning = ref true
 
 let opt_pruning=
   {optsync=true;
+   optdepr=false;
    optname="Rtauto Pruning";
    optkey=["Rtauto";"Pruning"];
    optread=(fun () -> !pruning);
diff --git a/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli
index 4d77a057..b236aa72 100644
--- a/plugins/rtauto/proof_search.mli
+++ b/plugins/rtauto/proof_search.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: proof_search.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 type form=
     Atom of int
   | Arrow of form * form
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 20b4c8f6..4a9a0e47 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -1,18 +1,15 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: refl_tauto.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 module Search = Explore.Make(Proof_search)
 
 open Util
 open Term
-open Termops
 open Names
 open Evd
 open Tacmach
@@ -39,7 +36,7 @@ let l_true_equals_true =
         [|data_constant "bool";data_constant "true"|]))
 
 let pos_constant =
-  Coqlib.gen_constant "refl_tauto" ["NArith";"BinPos"]
+  Coqlib.gen_constant "refl_tauto" ["Numbers";"BinNums"]
 
 let l_xI = lazy (pos_constant "xI")
 let l_xO = lazy (pos_constant "xO")
@@ -104,7 +101,7 @@ let rec make_form atom_env gls term =
   let cciterm=special_whd gls term  in
     match kind_of_term cciterm with
 	Prod(_,a,b) ->
-	  if not (dependent (mkRel 1) b) &&
+	  if not (Termops.dependent (mkRel 1) b) &&
 	    Retyping.get_sort_family_of
 	    (pf_env gls) (Tacmach.project gls) a = InProp
 	  then
@@ -144,7 +141,7 @@ let rec make_hyps atom_env gls lenv = function
   | (id,None,typ)::rest ->
       let hrec=
 	make_hyps atom_env gls (typ::lenv) rest in
-	if List.exists (dependent (mkVar id)) lenv ||
+	if List.exists (Termops.dependent (mkVar id)) lenv ||
 	  (Retyping.get_sort_family_of
 	     (pf_env gls) (Tacmach.project gls) typ <> InProp)
 	then
@@ -244,6 +241,7 @@ let verbose = ref false
 
 let opt_verbose=
   {optsync=true;
+   optdepr=false;
    optname="Rtauto Verbose";
    optkey=["Rtauto";"Verbose"];
    optread=(fun () -> !verbose);
@@ -255,6 +253,7 @@ let check = ref false
 
 let opt_check=
   {optsync=true;
+   optdepr=false;
    optname="Rtauto Check";
    optkey=["Rtauto";"Check"];
    optread=(fun () -> !check);
@@ -267,14 +266,13 @@ open Pp
 let rtauto_tac gls=
   Coqlib.check_required_library ["Coq";"rtauto";"Rtauto"];
   let gamma={next=1;env=[]} in
-  let gl=gls.it.evar_concl in
+  let gl=pf_concl gls in
   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
   let glf=make_form gamma gls gl in
-  let hyps=make_hyps gamma gls [gl]
-      (Environ.named_context_of_val gls.it.evar_hyps) 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 =
diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli
index 085a45a5..643433b0 100644
--- a/plugins/rtauto/refl_tauto.mli
+++ b/plugins/rtauto/refl_tauto.mli
@@ -1,12 +1,10 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id: refl_tauto.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (* raises Not_found if no proof is found *)
 
 type atom_env=