aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/string_syntax.ml
diff options
context:
space:
mode:
authorGuillaume Melquiond2014-03-10 16:39:53 +0100
committerGuillaume Melquiond2014-03-10 16:39:53 +0100
commit6a59faaddbefc0326a3071d81942ae4cc0dd0300 (patch)
treed39f7fab19d64cc81e3d835c7bf21e6c1cdc031b /plugins/syntax/string_syntax.ml
parent643e624909ecec7ba43326ff962b13c184991125 (diff)
Add missing lemmas: Rplus_eq_compat_r and Rplus_eq_reg_r.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions