aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorppedrot2013-06-12 21:07:40 +0000
committerppedrot2013-06-12 21:07:40 +0000
commitbea2a4f5fe5cab0abfc27492117c335a311a0c19 (patch)
treebbc934b7c6e0eb9baddf757b7f54d86776653f5d /dev
parent781f44a18cb5e2adbd0b2201d435e27938761af7 (diff)
Changing the type of Ltac values. Now they are toplevel generic
arguments. That way we will be able to define interpretation of tactics without referring to tactic values. Quite ad-hoc for now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16574 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions