+let add_to_trace cache t =
+ match t with
+ | Ast.NRef _ -> {cache with trace = t::cache.trace}
+ | Ast.NCic _ (* local candidate *)
+ | _ -> (*not an application *) cache
+
+(* not used
+let remove_from_trace cache t =
+ match t with
+ | Ast.NRef _ ->
+ (match cache.trace with
+ | _::tl -> {cache with trace = tl}
+ | _ -> assert false)
+ | Ast.NCic _ (* local candidate *)
+ | _ -> (*not an application *) cache *)
+