]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/disambiguation/multiPassDisambiguator.mli
arithmetics for λδ
[helm.git] / helm / software / components / disambiguation / multiPassDisambiguator.mli
index 4977a81d9cec60e9e370cce909d9164009bcb46f..41b79c9b025b2ea73761cf5937f62be39e841396 100644 (file)
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+val debug: bool ref
+
 (* the integer is an offset to be added to each location *)
 exception DisambiguationError of
  int *
@@ -48,6 +50,7 @@ val disambiguate_thing:
   expty: 'refined_thing option ->
   mk_implicit:(bool -> 'alias) ->
   description_of_alias:('alias -> string) ->
+  fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
   aliases:'alias DisambiguateTypes.Environment.t ->
   universe:'alias list
     DisambiguateTypes.Environment.t option ->