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.ml47719logplain
-rw-r--r--glob_term_to_relation.ml54454logplain
-rw-r--r--glob_term_to_relation.mli639logplain
-rw-r--r--glob_termops.ml24698logplain
-rw-r--r--glob_termops.mli4593logplain
-rw-r--r--indfun.ml30980logplain
-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.ml38551logplain
-rw-r--r--recdef.ml56272logplain
-rw-r--r--recdef.mli654logplain
-rw-r--r--recdef_plugin.mlpack142logplain