summaryrefslogtreecommitdiff
path: root/contrib/funind
ModeNameSize
-rw-r--r--indfun.ml14288logplain
-rw-r--r--indfun_common.ml10316logplain
-rw-r--r--indfun_common.mli1159logplain
-rw-r--r--indfun_main.ml45610logplain
-rw-r--r--invfun.ml3690logplain
-rw-r--r--new_arg_principle.ml52259logplain
-rw-r--r--new_arg_principle.mli935logplain
-rw-r--r--rawterm_to_relation.ml30860logplain
-rw-r--r--rawterm_to_relation.mli388logplain
-rw-r--r--rawtermops.ml15086logplain
-rw-r--r--rawtermops.mli3787logplain
-rw-r--r--tacinv.ml435586logplain
-rw-r--r--tacinvutils.ml7133logplain
-rw-r--r--tacinvutils.mli2425logplain