diff options
Diffstat (limited to 'coqprime/Coqprime/Permutation.v')
| -rw-r--r-- | coqprime/Coqprime/Permutation.v | 8 |
1 files changed, 4 insertions, 4 deletions
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 |