From fc2613e871dffffa788d90044a81598f671d0a3b Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 5 Jul 2012 16:56:16 +0000
Subject: ZArith + other : favor the use of modern names instead of compat
 notations

 - For instance, refl_equal --> eq_refl
 - Npos, Zpos, Zneg now admit more uniform qualified aliases
   N.pos, Z.pos, Z.neg.
 - A new module BinInt.Pos2Z with results about injections from
   positive to Z
 - A result about Z.pow pushed in the generic layer
 - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
 - Using tactic Z.le_elim instead of Zle_lt_or_eq
 - Some cleanup in ring, field, micromega
   (use of "Equivalence", "Proper" ...)
 - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
 - In ZMake and ZMake, functor parameters are now named NN and ZZ
   instead of N and Z for avoiding confusions

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/rtauto/Bintree.v     | 14 +++++++-------
 plugins/rtauto/refl_tauto.ml |  2 +-
 2 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'plugins/rtauto')

diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index 77f8f8345..8f024a15f 100644
--- a/plugins/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
@@ -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/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 8db267641..2fc80e1ff 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -33,7 +33,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 =
-- 
cgit v1.2.3