aboutsummaryrefslogtreecommitdiffstats
path: root/src/common/Maps.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/common/Maps.v')
-rw-r--r--src/common/Maps.v3
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.
+*)