aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
ModeNameSize
-rw-r--r--FunInd.v746logplain
-rw-r--r--Recdef.v1648logplain
-rw-r--r--functional_principles_proofs.ml56072logplain
-rw-r--r--functional_principles_proofs.mli664logplain
-rw-r--r--functional_principles_types.ml24685logplain
-rw-r--r--functional_principles_types.mli1492logplain
-rw-r--r--g_indfun.ml47827logplain
-rw-r--r--glob_term_to_relation.ml54981logplain
-rw-r--r--glob_term_to_relation.mli639logplain
-rw-r--r--glob_termops.ml20045logplain
-rw-r--r--glob_termops.mli3343logplain
-rw-r--r--indfun.ml32265logplain
-rw-r--r--indfun.mli532logplain
-rw-r--r--indfun_common.ml18095logplain
-rw-r--r--indfun_common.mli3899logplain
-rw-r--r--invfun.ml40159logplain
-rw-r--r--invfun.mli999logplain
-rw-r--r--recdef.ml56446logplain
-rw-r--r--recdef.mli550logplain
-rw-r--r--recdef_plugin.mlpack136logplain