and subst_magic pos env = function
| Ast.List0 (p, sep_opt)
| Ast.List1 (p, sep_opt) ->
- prerr_endline "1";
let rec_decls = CicNotationEnv.declarations_of_term p in
- prerr_endline "2";
let rec_values =
List.map (fun (n, _) -> CicNotationEnv.lookup_list env n) rec_decls
in
- prerr_endline "3";
let values = CicNotationUtil.ncombine rec_values in
- prerr_endline "4";
let sep =
match sep_opt with
| None -> []
| Some l -> [ Ast.Literal l; break; space ]
in
- prerr_endline "5";
let rec instantiate_list acc = function
| [] -> List.rev acc
| value_set :: [] ->