Strip the pointed instance names off of the default value in list expansion

This is required for reification to work, it seems

1 files changed, 1 insertions, 1 deletions

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index fe9aa8408..b34a5e322 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -1814,7 +1814,7 @@ Qed.
 Ltac expand_lists _ :=
   let default_for A :=
       match goal with
-      | _ => constr:(_ : pointed A)
+      | _ => (eval lazy in (_ : pointed A))
       | _ => let __ := match goal with _ => idtac "Warning: could not infer a default value for list type" A end in
              constr:(I : I)
       end in