aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssrmatching
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-08-18 09:50:17 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-02-20 10:03:05 +0100
commite21f70cc2b284a3cf489b16e0251492fb864cf1e (patch)
treea071e82af9ce82af1baff18ea46f06318462eb5c /plugins/ssrmatching
parentecc5658d7efd3a79a6309be6440d1005d30e6285 (diff)
Preliminary work before adding general support for patterns in notations II.
Reordering the maps for binders and terms while uninterpreting a notation the same way it will be at the time of interpreting a notation.
Diffstat (limited to 'plugins/ssrmatching')
0 files changed, 0 insertions, 0 deletions