diff options
| author | gareuselesinge | 2013-05-29 13:21:00 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-05-29 13:21:00 +0000 |
| commit | 9b3c26ae23606ceab42a44b5f9aa9d169016e564 (patch) | |
| tree | cfda25b8a3e2d0c2e3f63eeb34115deea6fed594 /plugins/syntax | |
| parent | 18373e78c9a0f171f193605ccb2556bb064b6e62 (diff) | |
Make ist (interp_sign) available to TACTIC EXTEND code
In order to do so I had to move the data base of tactics to
tacinterp (from tacintern).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16540 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions