summaryrefslogtreecommitdiff
path: root/plugins/funind
ModeNameSize
-rw-r--r--Recdef.v1688logplain
-rw-r--r--functional_principles_proofs.ml50664logplain
-rw-r--r--functional_principles_proofs.mli601logplain
-rw-r--r--functional_principles_types.ml23515logplain
-rw-r--r--functional_principles_types.mli855logplain
-rw-r--r--g_indfun.ml414895logplain
-rw-r--r--glob_term_to_relation.ml48528logplain
-rw-r--r--glob_term_to_relation.mli532logplain
-rw-r--r--glob_termops.ml21071logplain
-rw-r--r--glob_termops.mli4594logplain
-rw-r--r--indfun.ml29874logplain
-rw-r--r--indfun.mli512logplain
-rw-r--r--indfun_common.ml16197logplain
-rw-r--r--indfun_common.mli3207logplain
-rw-r--r--invfun.ml35816logplain
-rw-r--r--merge.ml38294logplain
-rw-r--r--recdef.ml48449logplain
-rw-r--r--recdef_plugin.mllib160logplain
-rw-r--r--vo.itarget10logplain