- coercion now requires an URI

[helm.git] / helm / ocaml / grafite_parser / grafiteDisambiguate.ml

diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
index 3c79cc0405806d1cd4b01f88b1eacbcbfbe56985..7b6b69d44479efacd2ecba74b1030e0e465acfa7 100644 (file)
--- a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
@@ -69,7 +69,7 @@ let disambiguate_lazy_term status_ref term =
 
 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
@@ -78,7 +78,7 @@ let disambiguate_pattern status_ref (wanted, hyp_paths, goal_path) =
        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) ->
@@ -233,6 +233,7 @@ let disambiguate_obj status obj =
 let disambiguate_command status =
   function
   | GrafiteAst.Alias _
+  | GrafiteAst.Coercion _
   | GrafiteAst.Default _
   | GrafiteAst.Drop _
   | GrafiteAst.Dump _
@@ -243,10 +244,7 @@ let disambiguate_command status =
   | 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)
+