aboutsummaryrefslogtreecommitdiff
path: root/dev/base_include
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-09-09 10:51:01 +0200
committerPierre-Marie Pédrot2016-09-11 15:18:39 +0200
commit5466267afa78cac5479a503338fbc57d77f05458 (patch)
tree46d441af7085b56b88b704c14276eae7bb055bba /dev/base_include
parenta6cd6948fa592f21b67916f423fe2adb62085492 (diff)
Move Ltac-specific components from G_proofs to G_ltac.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions