- Grammar for all obj commands ported to NG (let recs and inductives still need

- Grammar for all obj commands ported to NG (let recs and inductives still need
  implementation and raise assert false)
- New feature: every object can be both interactive or not, depending on the
  number of metavariables in the metasenv after disambiguation
- New objects are now put in the same namespace as old ones. The creation of
  aliases takes care of this by looking for new objects before looking for
  old ones. Note: this way the check is done twice, also when mapping
  aliases to terms. However, this is temporary code while the two "libraries"
  coexist.