1) mk_meta now returns also the index of the created meta

[helm.git] / helm / software / components / grafite_parser / grafiteDisambiguate.ml

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 027cde4a599d090787e1e2d86661577444df8e8f..323c8985edae63b82aac8b090a8258eaaa08d767 100644 (file)
--- 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 =