Imported Upstream version 8.4dfsgupstream/8.4dfsg

7 files changed, 15 insertions, 15 deletions

diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index 77f8f834..98dd257d 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-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -15,14 +15,14 @@ Open Scope positive_scope.
 Ltac clean := try (simpl; congruence).
 
 Lemma Gt_Psucc: forall p q,
-       (p ?= Psucc q) = Gt -> (p ?= q) = Gt.
+       (p ?= Pos.succ 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) = Gt.
+       (Pos.succ p ?= p) = Gt.
 Proof.
 intros. apply Pos.lt_gt, Pos.lt_succ_diag_r.
 Qed.
@@ -181,7 +181,7 @@ mkStore  {index:positive;contents:Tree}.
 Definition empty := mkStore xH Tempty.
 
 Definition push a  S :=
-mkStore (Psucc (index S)) (Tadd (index S) a (contents S)).
+mkStore (Pos.succ (index S)) (Tadd (index S) a (contents S)).
 
 Definition get i S := Tget i (contents S).
 
@@ -214,7 +214,7 @@ intros a S.
 rewrite Tget_Tadd.
 rewrite Psucc_Gt.
 intro W.
-change (get (Psucc (index S)) S =PNone).
+change (get (Pos.succ (index S)) S =PNone).
 apply get_Full_Gt; auto.
 apply Psucc_Gt.
 Qed.
@@ -248,7 +248,7 @@ forall x, get i S = PSome x ->
 Proof.
 intros i a S F x H.
 case_eq (i ?= index S);intro test.
-rewrite (Pcompare_Eq_eq _ _ test) in H.
+rewrite (Pos.compare_eq _ _ test) in H.
 rewrite (get_Full_Eq _ F) in H;congruence.
 rewrite <- H.
 rewrite (get_push_Full i a).
@@ -260,13 +260,13 @@ 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:=Psucc_not_one (index S)).
+simpl index in one;assert (h:=Pos.succ_not_1 (index S)).
 congruence.
 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 Psucc_not_one.
+simpl;intro H;injection H; intros _ ; apply Pos.succ_not_1.
 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 9cae7a44..3b596238 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-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \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 8d103d1b..96277e65 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-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \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 576f7d4e..c1e83004 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \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.mli b/plugins/rtauto/proof_search.mli
index 275e94cd..2adda33f 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-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \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 4a9a0e47..e8909f08 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-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -32,7 +32,7 @@ let data_constant =
   Coqlib.gen_constant "refl_tauto" ["Init";"Datatypes"]
 
 let l_true_equals_true =
-  lazy (mkApp(logic_constant "refl_equal",
+  lazy (mkApp(logic_constant "eq_refl",
         [|data_constant "bool";data_constant "true"|]))
 
 let pos_constant =
diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli
index 643433b0..e5fb646a 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-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)