let disambiguate_pattern status_ref (wanted, hyp_paths, goal_path) =
let interp path = Disambiguate.interpretate_path [] path in
- let goal_path = interp goal_path in
+ let goal_path = HExtlib.map_option interp goal_path in
let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
let wanted =
match wanted with
let wanted = disambiguate_lazy_term status_ref wanted in
Some wanted
in
- (wanted, hyp_paths ,goal_path)
+ (wanted, hyp_paths, goal_path)
let disambiguate_reduction_kind aliases_ref = function
| `Unfold (Some t) ->
let disambiguate_command status =
function
| GrafiteAst.Alias _
+ | GrafiteAst.Coercion _
| GrafiteAst.Default _
| GrafiteAst.Drop _
| GrafiteAst.Dump _
| GrafiteAst.Include _
| GrafiteAst.Interpretation _
- | GrafiteAst.Metadata _
| GrafiteAst.Notation _
| GrafiteAst.Qed _
| GrafiteAst.Render _
| GrafiteAst.Set _ as cmd ->
status,cmd
- | GrafiteAst.Coercion (loc, term, add_composites) ->
- let status_ref = ref status in
- let term = disambiguate_term ~context:[] status_ref ~-1 term in
- !status_ref, GrafiteAst.Coercion (loc,term,add_composites)
| GrafiteAst.Obj (loc,obj) ->
let status,obj = disambiguate_obj status obj in
status, GrafiteAst.Obj (loc,obj)
+