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/Root.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'coqprime/Coqprime/Root.v') diff --git a/coqprime/Coqprime/Root.v b/coqprime/Coqprime/Root.v index 321865ba1..4e74a4d2f 100644 --- a/coqprime/Coqprime/Root.v +++ b/coqprime/Coqprime/Root.v @@ -11,11 +11,11 @@ Proof that a polynomial has at most n roots ************************************************************************) -Require Import ZArith. -Require Import List. -Require Import UList. -Require Import Tactic. -Require Import Permutation. +Require Import Coq.ZArith.ZArith. +Require Import Coq.Lists.List. +Require Import Coqprime.UList. +Require Import Coqprime.Tactic. +Require Import Coqprime.Permutation. Open Scope Z_scope. -- cgit v1.2.3