diff options
| author | gmelquio | 2012-09-15 17:10:37 +0000 |
|---|---|---|
| committer | gmelquio | 2012-09-15 17:10:37 +0000 |
| commit | 730e25488e0f502359ed8c2a845b97bf0245d1e7 (patch) | |
| tree | d81f83c5c825e865ceb4fda85482e609bcebb58b /plugins/syntax/string_syntax.ml | |
| parent | 92616b9f660eaa2640964ca1925b05d37af70c8c (diff) | |
Port rewrites of tactic documentation from branch 8.4.
This encompasses commits r15183, r15190, r15243, r15262, r15276, r15277,
r15278, r15337. The merge did not go without troubles, but hopefully none
of the changes were lost in process.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15806 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions