diff options
| author | Pierre-Marie Pédrot | 2016-03-31 17:16:38 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-31 17:25:13 +0200 |
| commit | f5e85670b9c106fbde736654c32f4042c6a39d3f (patch) | |
| tree | 0401dc223bd6ef2ee0e60cb02c394a2fb9773139 /interp/notation.ml | |
| parent | c0aefc5323cb4393297adcaffd2967ab93ab815e (diff) | |
Moving the Tactic Notation entry parser from Pcoq to Tacentries.
Diffstat (limited to 'interp/notation.ml')
0 files changed, 0 insertions, 0 deletions