Remove old unused code

CertiCoq · Jan 27, 2025 · 6e59931 · 6e59931
1 parent e31583c
commit 6e59931
Show file tree

Hide file tree

Showing 51 changed files with 1 addition and 15,526 deletions.
diff --git a/libraries/MyPermutations.v b/libraries/MyPermutations.v
diff --git a/libraries/_CoqProject b/libraries/_CoqProject
@@ -3,5 +3,4 @@
 # libraries
 maps_util.v
 HashMap.v
-MyPermutations.v
 CpdtTactics.v
diff --git a/libraries/maps_util.v b/libraries/maps_util.v
@@ -8,14 +8,6 @@ Require Import Libraries.CpdtTactics Permutation ExtLib.Data.List Coq.NArith.Bin
 (* Utility library for Compcert's Maps *)
 
 
-(* Sections: 
-    DES: Useful facts about the PTree instance of Maps
-    EQMAP: map_get_r (equivalence relation on accessible content) and related
-    GETD : Get with default interpreation of None
-    EQDMAP: map_getd_r (equivalence relation with default interpretation of None) and related
-
- *)
-
 Module M := Maps.PTree.
 Definition var_dec := M.elt_eq.