diff options
Diffstat (limited to 'coqprime/Coqprime/ListAux.v')
| -rw-r--r-- | coqprime/Coqprime/ListAux.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/coqprime/Coqprime/ListAux.v b/coqprime/Coqprime/ListAux.v index 4ed154685..c3c9602bd 100644 --- a/coqprime/Coqprime/ListAux.v +++ b/coqprime/Coqprime/ListAux.v @@ -11,11 +11,11 @@ Auxillary functions & Theorems **********************************************************************) -Require Export Coq.Lists.List. -Require Export Coq.Arith.Arith. -Require Export Coqprime.Tactic. -Require Import Coq.Wellfounded.Inverse_Image. -Require Import Coq.Arith.Wf_nat. +Require Export List. +Require Export Arith. +Require Export Tactic. +Require Import Inverse_Image. +Require Import Wf_nat. (************************************** Some properties on list operators: app, map,... |