From 53112bb801cdcfb68e2b390f0935b9d3fa74ec04 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin <jasperh@cs.washington.edu>
Date: Thu, 22 Feb 2018 20:58:19 -0800
Subject: Change Implicit Arguments to Arguments in coqprime

---
 coqprime/Coqprime/Iterator.v    | 6 +++---
 coqprime/Coqprime/Permutation.v | 8 ++++----
 coqprime/Coqprime/UList.v       | 2 +-
 3 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'coqprime')

diff --git a/coqprime/Coqprime/Iterator.v b/coqprime/Coqprime/Iterator.v
index dbfde2c38..ed5261bcc 100644
--- a/coqprime/Coqprime/Iterator.v
+++ b/coqprime/Coqprime/Iterator.v
@@ -82,9 +82,9 @@ intros z n; generalize z; elim n; simpl; auto.
 Qed.
 
 End Iterator.
-Implicit Arguments iter [A B].
-Implicit Arguments progression [A].
-Implicit Arguments next_n [A].
+Arguments iter [A B].
+Arguments progression [A].
+Arguments next_n [A].
 Hint Unfold iter .
 Hint Unfold progression .
 Hint Unfold next_n .
diff --git a/coqprime/Coqprime/Permutation.v b/coqprime/Coqprime/Permutation.v
index 3a9b0860e..eb6969882 100644
--- a/coqprime/Coqprime/Permutation.v
+++ b/coqprime/Coqprime/Permutation.v
@@ -434,10 +434,10 @@ Hint Resolve permutation_app_swap.
    Implicits
    **************************************)
 
-Implicit Arguments permutation [A].
-Implicit Arguments split_one [A].
-Implicit Arguments all_permutations [A].
-Implicit Arguments permutation_dec [A].
+Arguments permutation [A] _ _.
+Arguments split_one [A] _.
+Arguments all_permutations [A] _.
+Arguments permutation_dec [A].
 
 (**************************************
    Permutation is compatible with map
diff --git a/coqprime/Coqprime/UList.v b/coqprime/Coqprime/UList.v
index 7dbd8562d..b787aad41 100644
--- a/coqprime/Coqprime/UList.v
+++ b/coqprime/Coqprime/UList.v
@@ -255,7 +255,7 @@ apply ulist_incl_length; auto.
 Qed.
 
 End UniqueList.
-Implicit Arguments ulist [A].
+Arguments ulist [A].
 Hint Constructors ulist .
 
 Theorem ulist_map:
-- 
cgit v1.2.3