let instantiate21 env precedence associativity l1 =
prerr_endline "instantiate21";
- let boxify = function
- | [t] -> t
- | tl -> Ast.Layout (Ast.Box (Ast.H, tl))
- in
let rec subst_singleton env t =
- boxify (subst env t)
+ CicNotationUtil.boxify (subst env t)
and subst env = function
| Ast.AttributedTerm (_, t) -> subst env t
| Ast.Variable var ->
| [] -> List.rev acc
| value_set :: [] ->
let env = CicNotationEnv.combine rec_decls value_set in
- instantiate_list ((boxify (subst env p)) :: acc) []
+ instantiate_list
+ ((CicNotationUtil.boxify (subst env p)) :: acc) []
| value_set :: tl ->
let env = CicNotationEnv.combine rec_decls value_set in
- instantiate_list ((boxify (subst env p @ sep)) :: acc) tl
+ instantiate_list
+ ((CicNotationUtil.boxify (subst env p @ sep)) :: acc) tl
in
- instantiate_list [] (List.rev values)
+ instantiate_list [] values
| Ast.Opt p ->
let opt_decls = CicNotationEnv.declarations_of_term p in
let env =