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
2684
log
plain
-rw-r--r--
FunctionalExtensionality.v
788
log
plain
-rw-r--r--
Subtac.v
66
log
plain
-rw-r--r--
Utils.v
2043
log
plain
-rw-r--r--
context.ml
910
log
plain
-rw-r--r--
context.mli
233
log
plain
-rw-r--r--
eterm.ml
5674
log
plain
-rw-r--r--
eterm.mli
1033
log
plain
-rw-r--r--
g_eterm.ml4
1345
log
plain
-rw-r--r--
g_subtac.ml4
4628
log
plain
-rw-r--r--
subtac.ml
8786
log
plain
-rw-r--r--
subtac.mli
131
log
plain
-rw-r--r--
subtac_cases.ml
73900
log
plain
-rw-r--r--
subtac_cases.mli
1669
log
plain
-rw-r--r--
subtac_coercion.ml
18291
log
plain
-rw-r--r--
subtac_coercion.mli
29
log
plain
-rw-r--r--
subtac_command.ml
15121
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_interp_fixpoint.ml
4615
log
plain
-rw-r--r--
subtac_interp_fixpoint.mli
686
log
plain
-rw-r--r--
subtac_obligations.ml
11905
log
plain
-rw-r--r--
subtac_obligations.mli
697
log
plain
-rw-r--r--
subtac_pretyping.ml
5429
log
plain
-rw-r--r--
subtac_pretyping.mli
381
log
plain
-rw-r--r--
subtac_pretyping_F.ml
22894
log
plain
-rw-r--r--
subtac_utils.ml
22013
log
plain
-rw-r--r--
subtac_utils.mli
3886
log
plain
d---------
test
317
log
plain