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 c3c9602bd..4ed154685 100644 --- a/coqprime/Coqprime/ListAux.v +++ b/coqprime/Coqprime/ListAux.v @@ -11,11 +11,11 @@ Auxillary functions & Theorems **********************************************************************) -Require Export List. -Require Export Arith. -Require Export Tactic. -Require Import Inverse_Image. -Require Import Wf_nat. +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. (************************************** Some properties on list operators: app, map,... |