let subterms = ref [] in
let map_term t =
subterms := t :: !subterms ;
- Ast.Implicit
+ Ast.Implicit `JustOne
in
- 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
and special_k = function
| Ast.AttributedTerm (_, t) -> aux t
| _ -> assert false
let add_magic m =
let name = Util.fresh_name () in
magic_map := (name, m) :: !magic_map;
- Ast.Variable (Ast.TermVar (name,None))
+ Ast.Variable (Ast.TermVar (name,Ast.Level 0))
in
let rec aux = function
| Ast.AttributedTerm (_, t) -> assert false
List.map2
(fun p t ->
match p, t with
- | Ast.Variable (Ast.TermVar (name,l)), _ ->
+ | 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)