aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-04-28 22:15:06 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-04-28 22:15:06 +0200
commit1c8ed18d5f67d7d5656342584b8dcf8a441cb87f (patch)
treece90c93341c58e82813da8b1a567ce6a3f3ed424 /theories/Reals
parent4f742e14441581ece247d33020055f15732f126b (diff)
Revert "Renaming allow_patvar flag of intern_gen into pattern_mode."
Diffstat (limited to 'theories/Reals')
0 files changed, 0 insertions, 0 deletions