diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-16 22:58:07 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-16 23:00:13 +0200 |
commit | ed1c4d01388bf11710b38f1c302d405233c24647 (patch) | |
tree | 0ffc730e786e65e03d253ac6d8d4e506c45bd751 /plugins/extraction/miniml.mli | |
parent | fd5898afa9a89ca61f87cdeca4ae982a024e4d4b (diff) |
Put the "change" tactic in the monad.
Diffstat (limited to 'plugins/extraction/miniml.mli')
0 files changed, 0 insertions, 0 deletions