aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/recdef_plugin.mllib
blob: c30ee212f5004617f1d9f7ed7a4fab855c684a50 (plain)
1
2
3
4
5
6
7
8
9
10
Indfun_common
Rawtermops
Recdef
Rawterm_to_relation
Functional_principles_proofs
Functional_principles_types
Invfun
Indfun
Merge
G_indfun