index
:
debian-coq
master
pristine-tar
upstream
Debian packaging for Coq
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
contrib
/
subtac
Mode
Name
Size
-rw-r--r--
FixSub.v
4266
log
plain
-rw-r--r--
FunctionalExtensionality.v
1359
log
plain
-rw-r--r--
Heq.v
823
log
plain
-rw-r--r--
Subtac.v
66
log
plain
-rw-r--r--
SubtacTactics.v
4990
log
plain
-rw-r--r--
Utils.v
1961
log
plain
-rw-r--r--
eterm.ml
6154
log
plain
-rw-r--r--
eterm.mli
1223
log
plain
-rw-r--r--
g_eterm.ml4
1345
log
plain
-rw-r--r--
g_subtac.ml4
5508
log
plain
-rw-r--r--
subtac.ml
6377
log
plain
-rw-r--r--
subtac.mli
92
log
plain
-rw-r--r--
subtac_cases.ml
85653
log
plain
-rw-r--r--
subtac_cases.mli
793
log
plain
-rw-r--r--
subtac_coercion.ml
18771
log
plain
-rw-r--r--
subtac_coercion.mli
29
log
plain
-rw-r--r--
subtac_command.ml
16851
log
plain
-rw-r--r--
subtac_command.mli
892
log
plain
-rw-r--r--
subtac_errors.ml
654
log
plain
-rw-r--r--
subtac_errors.mli
631
log
plain
-rw-r--r--
subtac_obligations.ml
14034
log
plain
-rw-r--r--
subtac_obligations.mli
1235
log
plain
-rw-r--r--
subtac_pretyping.ml
5561
log
plain
-rw-r--r--
subtac_pretyping.mli
381
log
plain
-rw-r--r--
subtac_pretyping_F.ml
22888
log
plain
-rw-r--r--
subtac_utils.ml
14258
log
plain
-rw-r--r--
subtac_utils.mli
4316
log
plain
d---------
test
317
log
plain