From aefb110d5ab007c7c70f56886ceabb2d72468e8c Mon Sep 17 00:00:00 2001
From: Alekandar Nanevski <aleks.nanevski@imdea.org>
Date: Fri, 1 Nov 2024 15:48:08 +0100
Subject: [PATCH] minor changes

---
 pcm/automap.v  | 2 +-
 pcm/unionmap.v | 1 -
 2 files changed, 1 insertion(+), 2 deletions(-)

diff --git a/pcm/automap.v b/pcm/automap.v
index fbbf15a..88d8474 100644
--- a/pcm/automap.v
+++ b/pcm/automap.v
@@ -79,7 +79,7 @@ Implicit Type i : @ctx K _ _ U.
 
 Inductive term := Pts of nat & T | Var of nat.
 
-(* interpretjtion function for elements *)
+(* interpretation function for elements *)
 Definition interp' i t :=
   match t with
     Pts n v => if onth (keyx i) n is Some k then @pts K _ _ _ k v else undef
diff --git a/pcm/unionmap.v b/pcm/unionmap.v
index 7253706..7262083 100644
--- a/pcm/unionmap.v
+++ b/pcm/unionmap.v
@@ -518,7 +518,6 @@ Proof. by split=>//; split=>[|[]]. Qed.
 HB.instance Definition _ := isUnion_map.Build K xpredT V (umap K V) umap_is_umc. 
 End UmapUMC.
 
-Set Printing All.
 (* if V is eqtype so is umap K V *)
 HB.instance Definition _ (K : ordType) (V : eqType) := 
   hasDecEq.Build (umap K V) (@union_map_eqP K xpredT V (umap K V)).