aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-07-05 12:21:34 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-07-05 12:21:34 +0000
commitd655986bc6d54c320a6ddd642cefde4a7f3088a9 (patch)
tree182ce5787d81586a9ebdb6cfd3f40bc6edaa28c0 /toplevel
parentc90d204c898ed8d7c28dd034782d3d868c85a926 (diff)
Fixes in rewriting by strategies (almost ready to be documented!):
- Proper parsing/globalization of strategy expressions. - Correct the error handling that gave rise to anomalies. - More informative error messages. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15513 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
0 files changed, 0 insertions, 0 deletions