Bug in the management of substitutions into auto corrected.

[helm.git] / helm / matita / matitaDisambiguator.ml

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index 01e85e0c45c0f4ba42bffa85c6d29902c955a275..bb7f2807dee162fe600850abe176d99dd214a773 100644 (file)
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+open MatitaTypes
+
 class parserr () =
   object
     method parseTerm = CicTextualParser2.parse_term
@@ -44,12 +46,12 @@ class disambiguator
             ~nonvars_button:enable_button_for_non_vars uris
 
         let interactive_interpretation_choice = chooseInterp
-        let input_or_locate_uri ~(title:string) =
-          (* TODO Zack: I try to avoid using this callback. I therefore assume
-           * that the presence of an identifier that can't be resolved via
-           * "locate" query is a syntax error *)
-          MatitaTypes.not_implemented
-            "MatitaDisambiguator: input_or_locate_uri callback"
+        let input_or_locate_uri ~(title:string) ?id =
+          (* Zack: I try to avoid using this callback. I therefore assume that
+          * the presence of an identifier that can't be resolved via "locate"
+          * query is a syntax error *)
+          let msg = match id with Some id -> id | _ -> "" in
+          raise (Unbound_identifier msg)
       end
     in
     let module Disambiguator = Disambiguate.Make (Callbacks) in