in
let rec aux t =
NotationUtil.visit_ast
+ ~clear_interpretation:true
~map_xref_option:(fun _ -> None)
~map_case_indty:(fun _ -> None)
~map_case_outtype:(fun _ _ -> None)
(* Debugging only *)
(*CSC: new NCicPp.status is the best I can do now *)
- let string_of_term = NotationPp.pp_term (new NCicPp.status)
- let string_of_pattern = NotationPp.pp_term (new NCicPp.status)
+ (*WR: can't guess a user id so I must use None *)
+ let string_of_term = NotationPp.pp_term (new NCicPp.status None)
+ let string_of_pattern = NotationPp.pp_term (new NCicPp.status None)
end
module M = PatternMatcher.Matcher (Pattern21)
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.IdentVar name), (Ast.Ident (s, `Ambiguous)) ->
name, (Env.StringType, Env.StringValue (Env.Ident s))
| _ -> assert false)
pl tl