aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
ModeNameSize
-rw-r--r--FunInd.v596logplain
-rw-r--r--Recdef.v1498logplain
-rw-r--r--functional_principles_proofs.ml55902logplain
-rw-r--r--functional_principles_proofs.mli664logplain
-rw-r--r--functional_principles_types.ml24685logplain
-rw-r--r--functional_principles_types.mli1432logplain
-rw-r--r--g_indfun.ml47701logplain
-rw-r--r--glob_term_to_relation.ml54419logplain
-rw-r--r--glob_term_to_relation.mli639logplain
-rw-r--r--glob_termops.ml24698logplain
-rw-r--r--glob_termops.mli4593logplain
-rw-r--r--indfun.ml30912logplain
-rw-r--r--indfun.mli532logplain
-rw-r--r--indfun_common.ml18142logplain
-rw-r--r--indfun_common.mli3899logplain
-rw-r--r--invfun.ml40491logplain
-rw-r--r--merge.ml38569logplain
-rw-r--r--recdef.ml56264logplain
-rw-r--r--recdef.mli654logplain
-rw-r--r--recdef_plugin.mlpack142logplain