aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorHugo Herbelin2014-11-23 12:27:19 +0100
committerHugo Herbelin2014-11-26 14:41:00 +0100
commita1a6d7b99eef5e6a671e5e6d057e46a6122e5e58 (patch)
tree108cd9d4644f9b610a6800eac6324d54455d1ec6 /lib
parent35fc7d7281688b248c55d3a8c2ed24b1c3fef38c (diff)
Experimenting always forcing convertibility on strict implicit arguments
in tactic unification.
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions