aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
ModeNameSize
-rw-r--r--FunInd.v0logplain
-rw-r--r--Recdef.v1465logplain
-rw-r--r--functional_principles_proofs.ml54389logplain
-rw-r--r--functional_principles_proofs.mli638logplain
-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.ml16143logplain
-rw-r--r--indfun_common.mli3641logplain
-rw-r--r--invfun.ml39399logplain
-rw-r--r--merge.ml38124logplain
-rw-r--r--recdef.ml53409logplain
-rw-r--r--recdef.mli658logplain
-rw-r--r--recdef_plugin.mlpack142logplain
-rw-r--r--vo.itarget20logplain