Skip to content

WIP ltac_tactics.v show `lazy_tc` does not work

Don't merge. Follow-up to !269 (comment 37145). Demonstrate that the existing code does not work as @robbertkrebbers (and any reasonable person) would think, by adding "redundant" parens that break everything.

$ time make -j4 TIMED=1 -k
COQDEP VFILES
COQDEP TESTFILES
COQC theories/proofmode/ltac_tactics.v
theories/proofmode/ltac_tactics (real: 2.59, user: 1.87, sys: 0.43, mem: 491692 ko)
COQC theories/proofmode/class_instances_bi.v
File "./theories/proofmode/class_instances_bi.v", line 1118, characters 2-63:
Error: Tactic failure: iSpecialize: (IAnon 4) not found.

Command exited with non-zero status 1
theories/proofmode/class_instances_bi (real: 7.71, user: 7.35, sys: 0.32, mem: 538288 ko)
make[2]: *** [theories/proofmode/class_instances_bi.vo] Error 1
make[1]: *** [all] Error 2
make: *** [all] Error 2

Merge request reports