- CicNotationEnv.term_of_value value
- | Ast.Magic m -> subst_magic last_box env m
- | Ast.Literal _ as t -> t
- | Ast.Layout l -> Ast.Layout (subst_layout last_box env l)
- | t -> CicNotationUtil.visit_ast (subst last_box env) t
- and subst_magic last_box env = function
+ [ CicNotationEnv.term_of_value value ]
+ | Ast.Magic m -> subst_magic env m
+ | Ast.Literal _ as t -> [ t ]
+ | Ast.Layout l -> [ Ast.Layout (subst_layout env l) ]
+ | t -> [ CicNotationUtil.visit_ast (subst_singleton env) t ]
+ and subst_magic env = function