summaryrefslogtreecommitdiff
path: root/plugins/funind
ModeNameSize
-rw-r--r--Recdef.v1465logplain
-rw-r--r--functional_principles_proofs.ml54361logplain
-rw-r--r--functional_principles_proofs.mli622logplain
-rw-r--r--functional_principles_types.ml23677logplain
-rw-r--r--functional_principles_types.mli1425logplain
-rw-r--r--g_indfun.ml48365logplain
-rw-r--r--glob_term_to_relation.ml49747logplain
-rw-r--r--glob_term_to_relation.mli613logplain
-rw-r--r--glob_termops.ml20893logplain
-rw-r--r--glob_termops.mli4336logplain
-rw-r--r--indfun.ml30518logplain
-rw-r--r--indfun.mli575logplain
-rw-r--r--indfun_common.ml16003logplain
-rw-r--r--indfun_common.mli3502logplain
-rw-r--r--invfun.ml39399logplain
-rw-r--r--merge.ml38124logplain
-rw-r--r--recdef.ml53364logplain
-rw-r--r--recdef.mli647logplain
-rw-r--r--recdef_plugin.mlpack142logplain
-rw-r--r--vo.itarget10logplain