aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
ModeNameSize
-rw-r--r--FunInd.v596logplain
-rw-r--r--Recdef.v1498logplain
-rw-r--r--functional_principles_proofs.ml55651logplain
-rw-r--r--functional_principles_proofs.mli673logplain
-rw-r--r--functional_principles_types.ml24422logplain
-rw-r--r--functional_principles_types.mli1446logplain
-rw-r--r--g_indfun.ml47784logplain
-rw-r--r--glob_term_to_relation.ml51885logplain
-rw-r--r--glob_term_to_relation.mli646logplain
-rw-r--r--glob_termops.ml23585logplain
-rw-r--r--glob_termops.mli4602logplain
-rw-r--r--indfun.ml30665logplain
-rw-r--r--indfun.mli577logplain
-rw-r--r--indfun_common.ml17399logplain
-rw-r--r--indfun_common.mli3969logplain
-rw-r--r--invfun.ml40030logplain
-rw-r--r--merge.ml38065logplain
-rw-r--r--recdef.ml55533logplain
-rw-r--r--recdef.mli666logplain
-rw-r--r--recdef_plugin.mlpack142logplain