Ioan asked me to :-)

searchAndDestroy.sh

@@ -1,4 +1,4 @@
-for file in `find theories/VLSM/Core/ELMO/ -maxdepth 1 -name 'UMO.v'`; do 
+for file in `find theories/VLSM/Core/ELMO/ -maxdepth 1 -name '*.v'`; do
    fline=`cat $file | head -n1`
    if [[ $fline == 'Set Default Proof Using "Type".' ]]; then
       echo $file

theories/VLSM/Core/ELMO/BaseELMO.v

@@ -1,3 +1,4 @@
+Set Default Proof Using "Type".
 From VLSM.Lib Require Import Itauto.
 From stdpp Require Import prelude finite.
 From VLSM.Lib Require Import EquationsExtras.

theories/VLSM/Core/ELMO/ELMO.v

@@ -1,3 +1,4 @@
+Set Default Proof Using "Type".
 From VLSM.Lib Require Import Itauto.
 From Coq Require Import FunctionalExtensionality Reals.
 From stdpp Require Import prelude finite.

theories/VLSM/Core/ELMO/MO.v

@@ -1,3 +1,4 @@
+Set Default Proof Using "Type".
 From VLSM.Lib Require Import Itauto.
 From Coq Require Import FunctionalExtensionality.
 From stdpp Require Import prelude finite.
@@ -713,7 +714,7 @@ Lemma state_suffix_totally_orders_valid_sent_messages :
       obs1 <*> MkObservation Send m1 <**> obs2 <*> MkObservation Send m2 <**> obs3 ->
     MO_msg_valid_alt_sends m ->
       state_suffix (state m1) (state m2) /\ state_suffix (state m2) (state m).
-Proof.
+Proof using P.
   intros m m1 m2 obs1 obs2 obs3 Heq Hvalid.
   red in Hvalid.
   assert (H2 :
@@ -1228,7 +1229,7 @@ Lemma unfold_rec_obs :
     rec_obs s ob
       <->
     ob ∈ obs s \/ exists m, MkObservation Receive m ∈ obs s /\ rec_obs (state m) ob.
-Proof using. clear. (* avoid unneccessary dependence on section variables *)
+Proof. clear -Message. (* avoid unneccessary dependence on section variables *)
   intros s ob; split.
   - induction 1.
     + by left; constructor.