aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ListUtil.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util/ListUtil.v')
-rw-r--r--src/Util/ListUtil.v2
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