diff options
| author | Pierre-Marie Pédrot | 2013-12-02 01:15:54 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2013-12-02 14:53:27 +0100 |
| commit | 85ed2504568ee06207546b1ac0660e9c559bca22 (patch) | |
| tree | 24f5c44a637a7cbeb8e6045c545fd9870f1f88d3 /plugins/xml/xmlcommand.ml | |
| parent | e0449b763d5854da2e7e48f4e92da779913a0347 (diff) | |
Writing [cut] tactic using the new monad.
Diffstat (limited to 'plugins/xml/xmlcommand.ml')
0 files changed, 0 insertions, 0 deletions