- map_unicode_to_tex:bool -> int ->
- #NCicCoercion.status ->
- NCic.metasenv -> NCic.substitution -> (* metasenv, substitution *)
+ metasenv:NCic.metasenv -> subst:NCic.substitution -> (* metasenv,substitution*)
+ map_unicode_to_tex:bool -> int -> #status ->