aboutsummaryrefslogtreecommitdiff
path: root/dev/include
diff options
context:
space:
mode:
authormsozeau2010-01-11 17:27:02 +0000
committermsozeau2010-01-11 17:27:02 +0000
commite61dee5744110f9316305aeaa4c363af7655a989 (patch)
tree8cc0757d3ed2ad15bfec2441f9c0a07478dbc03d /dev/include
parent6477ab0f7ea03a0563ca7ba2731d6aae1d3aa447 (diff)
Support "Local Obligation Tactic" (now the default in sections).
Update Numbers that was implicitely using [simpl_relation] instead of the default tactic [program_simpl]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12647 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions