~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp
in
let aux = function
- | G.Executable (_, G.Command (_, G.Obj (_, N.Inductive _))) as stm
+ | G.Executable (_, G.Command (_, G.Obj (_, N.Inductive _)))
+ | G.Executable (_, G.Command (_, G.Obj (_, N.Record _))) as stm
->
let hc = !Acic2content.hide_coercions in
if List.mem G.IPCoercions params then
enable_notations true;
Acic2content.hide_coercions := hc;
str
-(* FG: we disable notation for Inductive to avoid recursive notation *)
+(* FG: we disable notation for inductive types to avoid recursive notation *)
| G.Executable (_, G.Tactic _) as stm ->
let hc = !Acic2content.hide_coercions in
Acic2content.hide_coercions := false;