summaryrefslogtreecommitdiff
path: root/plugins/funind
ModeNameSize
-rw-r--r--Recdef.v1465logplain
-rw-r--r--functional_principles_proofs.ml53517logplain
-rw-r--r--functional_principles_proofs.mli623logplain
-rw-r--r--functional_principles_types.ml23056logplain
-rw-r--r--functional_principles_types.mli1425logplain
-rw-r--r--g_indfun.ml47936logplain
-rw-r--r--glob_term_to_relation.ml49167logplain
-rw-r--r--glob_term_to_relation.mli613logplain
-rw-r--r--glob_termops.ml20892logplain
-rw-r--r--glob_termops.mli4336logplain
-rw-r--r--indfun.ml29786logplain
-rw-r--r--indfun.mli403logplain
-rw-r--r--indfun_common.ml15993logplain
-rw-r--r--indfun_common.mli3501logplain
-rw-r--r--invfun.ml38469logplain
-rw-r--r--merge.ml37915logplain
-rw-r--r--recdef.ml52244logplain
-rw-r--r--recdef.mli647logplain
-rw-r--r--recdef_plugin.mllib160logplain
-rw-r--r--vo.itarget10logplain