Steel.Effect.Common: mark init_resolve_tac as a plugin

FStarLang · Sep 30, 2020 · 021bdeb · 021bdeb
1 parent 4592e12
commit 021bdeb
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/ulib/experimental/Steel.Effect.Common.fst b/ulib/experimental/Steel.Effect.Common.fst
@@ -1082,7 +1082,7 @@ let rec filter_goals (l:list goal) : Tac (list goal * list goal) =
       | App t _ -> if term_eq t (`squash) then hd::slgoals, loggoals else slgoals, loggoals
       | _ -> slgoals, loggoals
 
-[@@ resolve_implicits; framing_implicit]
+[@@ resolve_implicits; framing_implicit; plugin]
 let init_resolve_tac () : Tac unit =
   let slgs, loggs = filter_goals (goals()) in
   set_goals slgs;