aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorArnaud Spiwack2015-06-23 15:44:31 +0200
committerArnaud Spiwack2015-06-24 17:55:47 +0200
commit4a73e6b2bfb75451bcda7c74cf7478726a459799 (patch)
treed58157f7c092ee65911291d2e30afd144a829acb /plugins
parent9a1e80524e1650311b019fedbd7e774242d80ea4 (diff)
Add a corresponding field in `mutual_inductive_entry` (part 2).
The request for positivity to be assumed is honored.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions