From ed06a90f16fcf7d45672bbddf42efe4cc0efd4d4 Mon Sep 17 00:00:00 2001
From: gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 21 Nov 2011 17:03:52 +0000
Subject: theories/, plugins/ and test-suite/ ported to the Arguments
 vernacular

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14718 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/rtauto/Bintree.v | 50 ++++++++++++++++++++++++------------------------
 plugins/rtauto/Rtauto.v  |  4 ++--
 2 files changed, 27 insertions(+), 27 deletions(-)

(limited to 'plugins/rtauto')

diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index b34cf338b..77f8f8345 100644
--- a/plugins/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
@@ -34,7 +34,7 @@ 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.
@@ -288,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.
 
@@ -367,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 8b5e42447..9cae7a44e 100644
--- a/plugins/rtauto/Rtauto.v
+++ b/plugins/rtauto/Rtauto.v
@@ -73,7 +73,7 @@ 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.
 
@@ -161,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
-- 
cgit v1.2.3