diff --git a/src/core/Refiner.ml b/src/core/Refiner.ml
index 45b196f5a..0a55bdb49 100644
--- a/src/core/Refiner.ml
+++ b/src/core/Refiner.ml
@@ -709,6 +709,7 @@ struct
 
   let infer_nullary_ext : T.Chk.tac =
     T.Chk.rule ~name:"Univ.infer_nullary_ext" @@ function
+      (* TODO: another place to avoid this kind of matching *)
     | ElStable (`Ext (0,code ,`Global (Cof cof),bdry)) ->
       let* cof = RM.lift_cmp @@ Sem.cof_con_to_cof cof in
       let* () = Cof.assert_true cof in
@@ -852,6 +853,9 @@ struct
       let* tac = match tacs lbl, tp with
         | Some tac, _ -> RM.ret tac
         | None, ElStable (`Ext (0,_ ,`Global (Cof cof), _)) ->
+          (* This is a case where we can avoid matching on ElStable. 
+             We should instead check if the type is "judgmentally contractible" --- which can be implemented by a relatively simple type-directed algorithm.
+          *)
           let* cof = RM.lift_cmp @@ Sem.cof_con_to_cof cof in
           begin
             RM.lift_cmp @@ CmpM.test_sequent [] cof |>> function
diff --git a/src/frontend/Tactics.ml b/src/frontend/Tactics.ml
index c93a1e50a..cf14fa727 100644
--- a/src/frontend/Tactics.ml
+++ b/src/frontend/Tactics.ml
@@ -17,6 +17,8 @@ open Monad.Notation (RM)
 let is_total (sign : D.sign) =
   let rec go acc = function
     | D.Field (`User ["fib"],_,D.Clo ([],_)) -> RM.ret @@ acc
+
+    (* TODO: Let's avoid this kind of matching; maybe a good first step is even to make each field come equipped uniformly with a partial element. I favor that... *)
     | D.Field (lbl,(D.ElStable (`Ext (0,_,`Global (Cof cof),_)) as tp),sign_clo) ->
       let* cof = RM.lift_cmp @@ Sem.cof_con_to_cof cof in
       RM.abstract (lbl :> Ident.t) tp @@ fun v ->