diff options
| author | Hugo Herbelin | 2017-06-15 21:32:33 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-06-23 09:44:55 +0200 |
| commit | b4e1a902910cfab698fd5bdd2e9a18a28944c95e (patch) | |
| tree | f37472131788c59a61dfe73f65988aab768638fa /API/grammar_API.mli | |
| parent | d30ed5fe0694466f70eed51bc689cd0fa8c00da5 (diff) | |
In enter_one, not having exactly one goal is a fatal error of the monad.
Pointed out by PMP.
Diffstat (limited to 'API/grammar_API.mli')
0 files changed, 0 insertions, 0 deletions