X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=323c8985edae63b82aac8b090a8258eaaa08d767;hb=1c950d8cfe400f6b68eee7a67c555549db3a4d36;hp=027cde4a599d090787e1e2d86661577444df8e8f;hpb=b225178112c2c5ef1a717ac7e647d854d94b2e52;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 027cde4a5..323c8985e 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -234,6 +234,20 @@ let disambiguate_pattern
   (wanted, hyp_paths, goal_path)
 ;;
 
+type pattern = 
+  CicNotationPt.term Disambiguate.disambiguator_input option * 
+  (string * NCic.term) list * NCic.term option
+
+let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) =
+  let interp path = NCicDisambiguate.disambiguate_path 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 None -> None | Some x -> Some (text,prefix_len,x)
+  in
+   (wanted, hyp_paths, goal_path)
+;;
+
 let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
   | `Unfold (Some t) ->
       let t =