aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2013-11-09 13:28:38 +0100
committerGravatar Matthieu Sozeau <mattam@mattam.org>2014-05-06 09:58:55 +0200
commitde1f3069045e5b21804b9f58a3510999ef580c84 (patch)
treeceebbae8e291625754636bdfc6954775b1858bf7 /tactics/tactics.ml
parent7f59465dad8be7fa04b2e6b4ed0c49c38cd9e532 (diff)
Be defensive in univ/eq_instances, raise an anomaly on incompatible instances.
Diffstat (limited to 'tactics/tactics.ml')
0 files changed, 0 insertions, 0 deletions