fixing imports and changing to _CoqProject.

Author: Gregory Malecha

theories/Core/CmpDec.v

@@ -1,6 +1,6 @@
-Require Import Tactics.Consider.
-Require Import Bool.
-Require Import RelationClasses.
+Require Import Coq.Bool.Bool.
+Require Import Coq.Classes.RelationClasses.
+Require Import ExtLib.Tactics.Consider.
 
 Set Implicit Arguments.
 Set Strict Implicit.

theories/Core/Type.v

@@ -40,13 +40,19 @@ Section type.
     typeOk ->
     forall x y : T, equal x y -> proper x.
   Proof.
-    clear. intros. eapply only_proper in H0; intuition.
+    clear. intros.
+    match goal with
+    | H : equal _ _ |- _ => eapply only_proper in H
+    end; intuition.
   Qed.
   Global Polymorphic Instance proper_right :
     typeOk ->
     forall x y : T, equal x y -> proper y.
   Proof.
-    clear. intros. eapply only_proper in H0; intuition.
+    clear. intros.
+    match goal with
+    | H : equal _ _ |- _ => eapply only_proper in H
+    end; intuition.
   Qed.
 
 End type.

theories/Data/Graph/GraphAdjList.v

@@ -1,4 +1,4 @@
-Require Import List.
+Require Import ExtLib.Data.List.
 Require Import ExtLib.Data.Graph.Graph.
 Require Import ExtLib.Data.Graph.BuildGraph.
 Require Import ExtLib.Structures.Maps.

theories/Data/Monads/IdentityMonad.v

@@ -1,4 +1,4 @@
-Require Import Monad.
+Require Import ExtLib.Structures.Monad.
 
 Set Implicit Arguments.
 Set Maximal Implicit Insertion.

theories/Data/PreFun.v

@@ -1,4 +1,4 @@
-Require Import Morphisms.
+Require Import Coq.Classes.Morphisms.
 Require Import Coq.Relations.Relations.
 Require Import ExtLib.Structures.Proper.
 Require Import ExtLib.Core.Type.

theories/ExtLib.v

@@ -1 +1 @@
-Require Export Core.RelDec.
+Require Export ExtLib.Core.RelDec.

theories/Makefile

@@ -15,8 +15,8 @@ ARGS :=-R . ExtLib
 coq: Makefile.coq
 	$(MAKE) -f Makefile.coq
 
-Makefile.coq: Makefile $(VS)
-	@ coq_makefile $(ARGS) $(VS) -o Makefile.coq
+Makefile.coq: Makefile _CoqProject $(VS)
+	@ coq_makefile -f _CoqProject $(VS) -o Makefile.coq
 
 Makefile.test.coq: Makefile $(TVS)
 	coq_makefile $(ARGS) $(TVS) -o Makefile.test.coq

theories/Structures/MonadCont.v

@@ -1,4 +1,4 @@
-Require Import Monad.
+Require Import ExtLib.Structures.Monad.
 
 Set Implicit Arguments.
 Set Maximal Implicit Arguments.

theories/Structures/MonadExc.v

@@ -1,4 +1,4 @@
-Require Import Monad.
+Require Import ExtLib.Structures.Monad.
 
 Set Implicit Arguments.
 Set Maximal Implicit Arguments.

theories/Structures/MonadFix.v

@@ -1,4 +1,4 @@
-Require Import Monad.
+Require Import ExtLib.Structures.Monad.
 
 Set Implicit Arguments.
 Set Maximal Implicit Arguments.