Wrong category of error message when referring an undefined database #8
Description
If one types
Smpl Create foo.
smpl bar.The error message on line 3 is a syntax error, while it should be a context error. This disrupts the behavior of user-interfaces that perform some pre-parsing, like vsrocq.
It seems the fix should be to remove let _ = smpl_db_exists i in i replacing simply with i at https://github.com/uds-psl/smpl/blob/bd2d217eb32a7f0b27ef6c103d13f0b72e6e36d6/src/smpl.mlg#L227C24-L227C54.
Probably some more tests should also be added in commands that use the smpldb syntactic entry.