aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
ModeNameSize
-rw-r--r--Recdef.v1465logplain
-rw-r--r--functional_principles_proofs.ml52646logplain
-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.ml415868logplain
-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.ml27687logplain
-rw-r--r--indfun.mli403logplain
-rw-r--r--indfun_common.ml15740logplain
-rw-r--r--indfun_common.mli3405logplain
-rw-r--r--invfun.ml47052logplain
-rw-r--r--merge.ml37921logplain
-rw-r--r--recdef.ml50287logplain
-rw-r--r--recdef.mli647logplain
-rw-r--r--recdef_plugin.mllib160logplain
-rw-r--r--vo.itarget10logplain