diff options
| author | glondu | 2009-09-23 15:41:02 +0000 |
|---|---|---|
| committer | glondu | 2009-09-23 15:41:02 +0000 |
| commit | 492b5280384263a5dc9f5fb60c9c8d6bcbc8afce (patch) | |
| tree | 8f7235c2e72650c5af39f88bf8ed18eece8bf417 /plugins/interface/paths.ml | |
| parent | 287058532aefd848df5d83ee29707359672b626f (diff) | |
Ltac doc: only variables are accepted as message_token
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12352 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/interface/paths.ml')
0 files changed, 0 insertions, 0 deletions