From dbe09dd5bfc2595cb9fd96725d87d9a729cd0247 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 10 Mar 2016 13:45:37 -0500 Subject: Absolutize Coqprime imports Used ```bash cd coqprime make -kj10 cd Coqprime git ls-files "*.v" | xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Coqprime ``` --- coqprime/Coqprime/ListAux.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'coqprime/Coqprime/ListAux.v') 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,... -- cgit v1.2.3