type ('term,'obj) command =
| Index of loc * 'term option (* key *) * UriManager.uri (* value *)
type ('term,'obj) command =
| Index of loc * 'term option (* key *) * UriManager.uri (* value *)
| UnificationHint of loc * CicNotationPt.term * int (* term, precedence *)
| NObj of loc * CicNotationPt.term CicNotationPt.obj
| NUnivConstraint of loc * bool * NUri.uri * NUri.uri
| UnificationHint of loc * CicNotationPt.term * int (* term, precedence *)
| NObj of loc * CicNotationPt.term CicNotationPt.obj
| NUnivConstraint of loc * bool * NUri.uri * NUri.uri