summaryrefslogtreecommitdiff
path: root/plugins/subtac
ModeNameSize
-rw-r--r--eterm.ml8004logplain
-rw-r--r--eterm.mli1701logplain
-rw-r--r--g_subtac.ml46103logplain
-rw-r--r--subtac.ml7803logplain
-rw-r--r--subtac.mli92logplain
-rw-r--r--subtac_cases.ml76162logplain
-rw-r--r--subtac_cases.mli801logplain
-rw-r--r--subtac_classes.ml6603logplain
-rw-r--r--subtac_classes.mli1169logplain
-rw-r--r--subtac_coercion.ml16422logplain
-rw-r--r--subtac_coercion.mli90logplain
-rw-r--r--subtac_command.ml19693logplain
-rw-r--r--subtac_command.mli1521logplain
-rw-r--r--subtac_errors.ml650logplain
-rw-r--r--subtac_errors.mli631logplain
-rw-r--r--subtac_obligations.ml20761logplain
-rw-r--r--subtac_obligations.mli2690logplain
-rw-r--r--subtac_plugin.mllib181logplain
-rw-r--r--subtac_pretyping.ml5040logplain
-rw-r--r--subtac_pretyping.mli684logplain
-rw-r--r--subtac_pretyping_F.ml24755logplain
-rw-r--r--subtac_utils.ml15099logplain
-rw-r--r--subtac_utils.mli4470logplain
d---------test351logplain