aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/glob_term_to_relation.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-11-08 10:20:08 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-11-09 12:39:15 +0100
commitd69e4f55757c9066b0ae600d14ef89de3c8eb07d (patch)
tree1e3cacf04376924517b0b4be2144ca51f6f60f23 /plugins/funind/glob_term_to_relation.mli
parent0d81e80a09db7d352408be4dfc5ba263f6ed98ef (diff)
ssr: fill_occ_pattern: return valid ustate even if no match (fix #6106)
Diffstat (limited to 'plugins/funind/glob_term_to_relation.mli')
0 files changed, 0 insertions, 0 deletions