aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
ModeNameSize
-rw-r--r--Recdef.v1465logplain
-rw-r--r--functional_principles_proofs.ml55413logplain
-rw-r--r--functional_principles_proofs.mli652logplain
-rw-r--r--functional_principles_types.ml24430logplain
-rw-r--r--functional_principles_types.mli1433logplain
-rw-r--r--g_indfun.ml48407logplain
-rw-r--r--glob_term_to_relation.ml51705logplain
-rw-r--r--glob_term_to_relation.mli637logplain
-rw-r--r--glob_termops.ml21460logplain
-rw-r--r--glob_termops.mli4244logplain
-rw-r--r--indfun.ml31370logplain
-rw-r--r--indfun.mli584logplain
-rw-r--r--indfun_common.ml17209logplain
-rw-r--r--indfun_common.mli3948logplain
-rw-r--r--invfun.ml40591logplain
-rw-r--r--merge.ml38679logplain
-rw-r--r--recdef.ml55455logplain
-rw-r--r--recdef.mli664logplain
-rw-r--r--recdef_plugin.mlpack142logplain
-rw-r--r--vo.itarget10logplain