summaryrefslogtreecommitdiff
path: root/plugins/funind
ModeNameSize
-rw-r--r--Recdef.v1688logplain
-rw-r--r--functional_principles_proofs.ml50860logplain
-rw-r--r--functional_principles_proofs.mli601logplain
-rw-r--r--functional_principles_types.ml23485logplain
-rw-r--r--functional_principles_types.mli855logplain
-rw-r--r--g_indfun.ml414951logplain
-rw-r--r--glob_term_to_relation.ml48753logplain
-rw-r--r--glob_term_to_relation.mli532logplain
-rw-r--r--glob_termops.ml21161logplain
-rw-r--r--glob_termops.mli4594logplain
-rw-r--r--indfun.ml30016logplain
-rw-r--r--indfun.mli512logplain
-rw-r--r--indfun_common.ml16351logplain
-rw-r--r--indfun_common.mli3207logplain
-rw-r--r--invfun.ml35870logplain
-rw-r--r--merge.ml38372logplain
-rw-r--r--recdef.ml49429logplain
-rw-r--r--recdef_plugin.mllib160logplain
-rw-r--r--vo.itarget10logplain