diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-04-17 18:52:33 -0400 |
|---|---|---|
| committer |  jadephilipoom <jade.philipoom@gmail.com> | 2018-04-18 03:43:32 -0400 |
| commit | f2ef2c85530035b60d9071abf256da37e84858bf (patch) | |
| tree | 0c5a0385d61e4442e5afd521b5f215a0c975341f /src | |
| parent | c574d7ecbd4633ddb3116a71d49ec180526ee8dc (diff) | |
Actually display the error messages from pipeline failures
See https://github.com/coq/coq/issues/7291 and
https://github.com/mit-plv/fiat-crypto/issues/349#issuecomment-382180578
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index ab1580026..457838787 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -7072,7 +7072,11 @@ Ltac vm_compute_lhs_reflexivity := lazymatch goal with | [ |- ?LHS = ?RHS ] => let x := (eval vm_compute in LHS) in - unify RHS x; + (* we cannot use the unify tactic, which just gives "not + unifiable" as the error message, because we want to see the + terms that were not unifable. See also + COQBUG(https://github.com/coq/coq/issues/7291) *) + let _unify := constr:(ltac:(reflexivity) : RHS = x) in vm_cast_no_check (eq_refl x) end. |