summaryrefslogtreecommitdiff
path: root/plugins/subtac
ModeNameSize
-rw-r--r--eterm.ml8052logplain
-rw-r--r--eterm.mli1640logplain
-rw-r--r--g_subtac.ml45995logplain
-rw-r--r--subtac.ml7941logplain
-rw-r--r--subtac.mli92logplain
-rw-r--r--subtac_cases.ml76082logplain
-rw-r--r--subtac_cases.mli734logplain
-rw-r--r--subtac_classes.ml6876logplain
-rw-r--r--subtac_classes.mli1105logplain
-rw-r--r--subtac_coercion.ml16292logplain
-rw-r--r--subtac_coercion.mli90logplain
-rw-r--r--subtac_command.ml19973logplain
-rw-r--r--subtac_command.mli1507logplain
-rw-r--r--subtac_errors.ml650logplain
-rw-r--r--subtac_errors.mli631logplain
-rw-r--r--subtac_obligations.ml22642logplain
-rw-r--r--subtac_obligations.mli2692logplain
-rw-r--r--subtac_plugin.mllib181logplain
-rw-r--r--subtac_pretyping.ml4914logplain
-rw-r--r--subtac_pretyping.mli688logplain
-rw-r--r--subtac_pretyping_F.ml24489logplain
-rw-r--r--subtac_utils.ml14699logplain
-rw-r--r--subtac_utils.mli4273logplain
d---------test351logplain