Merge pull request #19 from coq-community/compat-8.11

Compat 8.11

_CoqProject

@@ -2,7 +2,7 @@
 
 -arg -w -arg +default
 
-theories/Aux.v
+theories/AuxLib.v
 theories/Cover.v
 theories/HeightPred.v
 theories/Ordered.v

theories/Aux.v → theories/AuxLib.v

@@ -14,7 +14,7 @@
 (* 02110-1301 USA                                                     *)
 
 (**
-    Proof of Huffman algorithm: Aux.v
+    Proof of Huffman algorithm: AuxLib.v
 
     Auxiliary functions & theorems
 

theories/Code.v

@@ -26,7 +26,7 @@
 *)
 
 Require Bool.Bool.
-From Huffman Require Export Aux.
+From Huffman Require Export AuxLib.
 From Huffman Require Export Permutation.
 From Huffman Require Export UniqueKey.
 From Huffman Require Export Frequency.

theories/Frequency.v

@@ -23,7 +23,7 @@
     Initial author: [email protected] (2003)
 *)
 
-From Huffman Require Import Aux.
+From Huffman Require Import AuxLib.
 Require Import List.
 From Huffman Require Import UniqueKey.
 From Huffman Require Import Permutation.

theories/HeightPred.v

@@ -24,7 +24,7 @@
     Initial author: [email protected] (2003)
 *)
 
-From Huffman Require Export Aux.
+From Huffman Require Export AuxLib.
 From Huffman Require Export OrderedCover.
 From Huffman Require Export WeightTree.
 Require Import ArithRing.

theories/Ordered.v

@@ -24,7 +24,7 @@
 *)
 
 From Huffman Require Export Permutation.
-From Huffman Require Export Aux.
+From Huffman Require Export AuxLib.
 
 Section ordered.
 Variable A : Type.

theories/PBTree.v

@@ -26,7 +26,7 @@
 *)
 
 Require Import List.
-From Huffman Require Import Aux.
+From Huffman Require Import AuxLib.
 From Huffman Require Import Code.
 From Huffman Require Import Build.
 From Huffman Require Import ISort.

theories/PBTree2BTree.v

@@ -23,7 +23,7 @@
     Initial author: [email protected] (2003)
 *)
 
-From Huffman Require Export Aux.
+From Huffman Require Export AuxLib.
 From Huffman Require Export Code.
 From Huffman Require Export Build.
 From Huffman Require Export ISort.

theories/Permutation.v

@@ -23,7 +23,7 @@
     Initial author: [email protected] (2003)
 *)
 
-From Huffman Require Export Aux.
+From Huffman Require Export AuxLib.
 
 Section permutation.
 Variable A : Type.

theories/UniqueKey.v

@@ -21,7 +21,7 @@
     Initial author: [email protected] (2003)
 *)
 
-From Huffman Require Export Aux.
+From Huffman Require Export AuxLib.
 From Huffman Require Export Permutation.
 From Huffman Require Export UList.
 

theories/dune

@@ -2,5 +2,4 @@
  (name Huffman)
  (public_name coq-huffman.Huffman)
  (synopsis "Coq proof of the correctness of the Huffman coding algorithm")
- (libraries coq.plugins.extraction)
  (modules :standard))