minor changes

imdea-software · Nov 1, 2024 · aefb110 · aefb110
1 parent ad2b680
commit aefb110
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 2 deletions.
diff --git 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
@@ -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)).