summaryrefslogtreecommitdiff
path: root/plugins/funind
ModeNameSize
-rw-r--r--Recdef.v1465logplain
-rw-r--r--functional_principles_proofs.ml52694logplain
-rw-r--r--functional_principles_proofs.mli601logplain
-rw-r--r--functional_principles_types.ml22175logplain
-rw-r--r--functional_principles_types.mli821logplain
-rw-r--r--g_indfun.ml415889logplain
-rw-r--r--glob_term_to_relation.ml48239logplain
-rw-r--r--glob_term_to_relation.mli562logplain
-rw-r--r--glob_termops.ml20892logplain
-rw-r--r--glob_termops.mli4334logplain
-rw-r--r--indfun.ml27745logplain
-rw-r--r--indfun.mli403logplain
-rw-r--r--indfun_common.ml15740logplain
-rw-r--r--indfun_common.mli3405logplain
-rw-r--r--invfun.ml47095logplain
-rw-r--r--merge.ml37901logplain
-rw-r--r--recdef.ml50335logplain
-rw-r--r--recdef.mli647logplain
-rw-r--r--recdef_plugin.mllib160logplain
-rw-r--r--vo.itarget10logplain