aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
ModeNameSize
-rw-r--r--FunInd.v596logplain
-rw-r--r--Recdef.v1498logplain
-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.mli1342logplain
-rw-r--r--g_indfun.ml47677logplain
-rw-r--r--glob_term_to_relation.ml54641logplain
-rw-r--r--glob_term_to_relation.mli639logplain
-rw-r--r--glob_termops.ml20045logplain
-rw-r--r--glob_termops.mli3343logplain
-rw-r--r--indfun.ml31074logplain
-rw-r--r--indfun.mli532logplain
-rw-r--r--indfun_common.ml18095logplain
-rw-r--r--indfun_common.mli3899logplain
-rw-r--r--invfun.ml40009logplain
-rw-r--r--invfun.mli849logplain
-rw-r--r--recdef.ml56272logplain
-rw-r--r--recdef.mli550logplain
-rw-r--r--recdef_plugin.mlpack136logplain