Fix proof breakage by not importing String module, update Iris

diaframe/lib/own/validity_tactics.v

@@ -64,7 +64,7 @@ Proof.
 Qed.
 
 Ltac iCombineOwn_tac' Hs_raw destructstr := 
-  let Hs := words Hs_raw in
+  let Hs := String.words Hs_raw in
   let get_hyp_type Hname := 
     let Δ := match goal with | |- environments.envs_entails ?Δ _ => Δ end in
     let lookup := eval pm_eval in (environments.envs_lookup (INamed Hname) Δ) in