summaryrefslogtreecommitdiff
path: root/plugins/funind
ModeNameSize
-rw-r--r--Recdef.v1465logplain
-rw-r--r--functional_principles_proofs.ml53466logplain
-rw-r--r--functional_principles_proofs.mli623logplain
-rw-r--r--functional_principles_types.ml22838logplain
-rw-r--r--functional_principles_types.mli869logplain
-rw-r--r--g_indfun.ml416061logplain
-rw-r--r--glob_term_to_relation.ml48402logplain
-rw-r--r--glob_term_to_relation.mli613logplain
-rw-r--r--glob_termops.ml20892logplain
-rw-r--r--glob_termops.mli4334logplain
-rw-r--r--indfun.ml29594logplain
-rw-r--r--indfun.mli403logplain
-rw-r--r--indfun_common.ml15750logplain
-rw-r--r--indfun_common.mli3441logplain
-rw-r--r--invfun.ml38448logplain
-rw-r--r--merge.ml37901logplain
-rw-r--r--recdef.ml52148logplain
-rw-r--r--recdef.mli647logplain
-rw-r--r--recdef_plugin.mllib160logplain
-rw-r--r--vo.itarget10logplain