diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2014-12-16 12:48:08 +0100 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2014-12-16 12:48:08 +0100 |
| commit | 37ed28dfe253615729763b5d81a533094fb5425e (patch) | |
| tree | 2940422acc2be9d34585766993d717d52cb46886 /library/declaremods.ml | |
| parent | 8bda62e798c4e89c8c3f9406327899e394f7be0f (diff) | |
Error messages of Searchxxx are coherent with goal selector.
If a goal is given and wrong, exception is raised. If no goal is
given, then goal 1 is tried but no failure if goal 1 does not exist,
just fall back to gloab env.
Diffstat (limited to 'library/declaremods.ml')
0 files changed, 0 insertions, 0 deletions