- let rec aux t = CicNotationUtil.visit_ast ~special_k map_term t
+ let rec aux t =
+ CicNotationUtil.visit_ast
+ ~map_xref_option:(fun _ -> None)
+ ~map_case_indty:(fun _ -> None)
+ ~map_case_outtype:(fun _ _ -> None)
+ ~special_k map_term t
let add_magic m =
let name = Util.fresh_name () in
magic_map := (name, m) :: !magic_map;
let add_magic m =
let name = Util.fresh_name () in
magic_map := (name, m) :: !magic_map;
- Ast.Variable (Ast.TermVar name), _ ->
- name, (Env.TermType, Env.TermValue t)
+ | Ast.Variable (Ast.TermVar (name,(Ast.Self l|Ast.Level l))), _ ->
+ name, (Env.TermType l, Env.TermValue t)
| Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) ->
name, (Env.NumType, Env.NumValue s)
| Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) ->
| Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) ->
name, (Env.NumType, Env.NumValue s)
| Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) ->