Add constr_fail and constr_fail_with

Rather than taking the convention that failures during constr
construction emit a type error from `I : I` with the actual error
message `idtac`d above them (because Coq has no way to emit multiple
things on stderr), we instead factor everything through a new
`constr_fail` or `constr_fail_with msg_tac`, which emit more helpful
messages instructing the user to look in `*coq*` or to use `Fail`/`try`
to see the more informative error message.  When we can make our own
version that does both `idtac` and `fail` (c.f.
https://github.com/coq/coq/issues/3913), then we can do something a bit
more sane, hopefully.

1 files changed, 2 insertions, 2 deletions

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index ac6575a4f..b7a5292d8 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -12,6 +12,7 @@ Require Export Crypto.Util.Tactics.BreakMatch.
 Require Export Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Util.Tactics.SpecializeBy.
 Require Import Crypto.Util.Tactics.RewriteHyp.
+Require Import Crypto.Util.Tactics.ConstrFail.
 Import ListNotations.
 Local Open Scope list_scope.
 
@@ -1910,8 +1911,7 @@ Ltac expand_lists _ :=
   let default_for A :=
       match goal with
       | _ => (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)
+      | _ => constr_fail_with ltac:(fun _ => idtac "Warning: could not infer a default value for list type" A)
       end in
   let T := lazymatch goal with |- _ = _ :> ?T => T end in
   let v := fresh in