diff options
Diffstat (limited to 'src/common/Maps.v')
-rw-r--r-- | src/common/Maps.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/common/Maps.v b/src/common/Maps.v index f0f264d..13ca276 100644 --- a/src/common/Maps.v +++ b/src/common/Maps.v @@ -17,7 +17,7 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -Set Implicit Arguments. +(*Set Implicit Arguments. Require Export compcert.lib.Maps. @@ -62,3 +62,4 @@ Definition traverse (A B : Type) (f : positive -> A -> res B) m := xtraverse f m Definition traverse1 (A B : Type) (f : A -> res B) := traverse (fun _ => f). End PTree. +*) |