add | 10 to new Reflexive, Symmetric, and Transitive instances

mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps

MIT License

42 stars 24 forks source link

add | 10 to new Reflexive, Symmetric, and Transitive instances #29

Closed jadephilipoom closed 4 years ago

jadephilipoom commented 4 years ago

As per https://github.com/mit-plv/coqutil/pull/28#discussion_r441182054

samuelgruetter commented 4 years ago

@JasonGross thanks for pointing out the issue. Does adding this Reflexive instance (with or without the | 10) affect the amount of time reflexivity needs to fail?

JasonGross commented 4 years ago

It only has an impact if your goal is something like ?R x x. It does not impact things for goals which have no evars (and which there are no evars generated during whatever tactic you're using)