aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
ModeNameSize
-rw-r--r--FunInd.v746logplain
-rw-r--r--Recdef.v1648logplain
-rw-r--r--functional_principles_proofs.ml56142logplain
-rw-r--r--functional_principles_proofs.mli664logplain
-rw-r--r--functional_principles_types.ml25039logplain
-rw-r--r--functional_principles_types.mli1492logplain
-rw-r--r--g_indfun.ml47881logplain
-rw-r--r--glob_term_to_relation.ml54982logplain
-rw-r--r--glob_term_to_relation.mli639logplain
-rw-r--r--glob_termops.ml20166logplain
-rw-r--r--glob_termops.mli3326logplain
-rw-r--r--indfun.ml32375logplain
-rw-r--r--indfun.mli537logplain
-rw-r--r--indfun_common.ml18055logplain
-rw-r--r--indfun_common.mli3848logplain
-rw-r--r--invfun.ml40101logplain
-rw-r--r--invfun.mli988logplain
-rw-r--r--recdef.ml56410logplain
-rw-r--r--recdef.mli550logplain
-rw-r--r--recdef_plugin.mlpack136logplain