diff options
| author | Pierre-Marie Pédrot | 2014-08-18 00:02:45 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-08-18 01:15:43 +0200 |
| commit | 243ffa4b928486122075762da6ce8da707e07daf (patch) | |
| tree | 3870e1b1d3059ba13158a73df7c5f3b300e504ce /pretyping/typeclasses_errors.ml | |
| parent | 6dd9e003c289a79b0656e7c6f2cc59935997370c (diff) | |
Moving the TacExtend node from atomic to plain tactics.
Also taking advantage of the change to rename it into TacML. Ultimately
should allow ML tactic to return values.
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions