more cleanup

bedrock2/src/bedrock2/FE310CSemantics.v

@@ -62,7 +62,7 @@ Section WithParameters.
   Qed.
 
   Global Instance ext_spec : Semantics.ExtSpec := deleakaged_ext_spec.
-  Global Instance ext_spec_ok : Semantics.ext_spec.ok sem_ext_spec := deleakaged_ext_spec_ok.
+  Global Instance ext_spec_ok : Semantics.ext_spec.ok ext_spec := deleakaged_ext_spec_ok.
 
   Global Instance locals: Interface.map.map String.string word := SortedListString.map _.
   Global Instance env: Interface.map.map String.string (list String.string * list String.string * cmd) :=

bedrock2/src/bedrock2/MetricLeakageSemantics.v

@@ -2,6 +2,7 @@ Require Import coqutil.sanity coqutil.Byte.
 Require Import coqutil.Tactics.fwd.
 Require Import coqutil.Map.Properties.
 Require coqutil.Map.SortedListString.
+Require Import coqutil.Z.Lia.
 Require Import bedrock2.Syntax coqutil.Map.Interface coqutil.Map.OfListWord.
 Require Import BinIntDef coqutil.Word.Interface coqutil.Word.Bitwidth.
 Require Export bedrock2.Memory.
@@ -261,8 +262,6 @@ Module exec. Section WithParams.
         eauto 10.
   Qed.
 
-    Require Import coqutil.Z.Lia.
-
   Lemma eval_expr_extends_trace :
     forall e0 m l mc k v mc' k',
     eval_expr m l e0 k mc = Some (v, k', mc') ->
@@ -640,7 +639,7 @@ Section WithParams.
       destruct IHarges as (mc'' & IH). rewrite IH. eauto.
   Qed.
 
-  Definition deleakaged_ext_spec :=
+  Definition deleakaged_ext_spec : Semantics.ExtSpec :=
     fun t mGive a args post => ext_spec t mGive a args (fun mReceive resvals klist => post mReceive resvals).
 
   Lemma deleakaged_ext_spec_ok {ext_spec_ok: ext_spec.ok ext_spec}:
@@ -652,7 +651,8 @@ Section WithParams.
   Qed.    
 
   Context (e: env).
-  Instance sem_ext_spec : Semantics.ExtSpec := deleakaged_ext_spec.
+  Existing Instance deleakaged_ext_spec.
+  Existing Instance deleakaged_ext_spec_ok.
 
   Lemma to_plain_exec: forall c t m l post,
       Semantics.exec e c t m l post ->