aboutsummaryrefslogtreecommitdiff
path: root/dev/include
diff options
context:
space:
mode:
authorPierre Courtieu2014-12-12 18:20:46 +0100
committerPierre Courtieu2014-12-12 18:21:50 +0100
commited89c1ee0d24d0e4356e77561bab4822125db057 (patch)
tree46e68f141580235481fb06dd2206abf516a70009 /dev/include
parent607503b28fca50f4b76b2237d5ca13802b8252fa (diff)
Searchxxx now interpret patterns in goal environment if any.
This makes such things work: x:nat h: x = 3 ================ True Search x.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions