(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.      
     \ /   This software is distributed as is, NO WARRANTY.     
      V_______________________________________________________________ *)

(* $Id$ *)

exception DisambiguationError of
 int *
 ((Stdpp.location list * string * string) list *
  (DisambiguateTypes.domain_item * string) list *
  (Stdpp.location * string) Lazy.t * bool) list list

val disambiguate_term :
  context:NCic.context ->
  metasenv:NCic.metasenv -> 
  subst:NCic.substitution ->
  ?goal:int ->
  aliases:NCic.term DisambiguateTypes.environment ->
  universe:NCic.term DisambiguateTypes.multiple_environment option ->
  CicNotationPt.term Disambiguate.disambiguator_input ->
  ((DisambiguateTypes.domain_item * 
    NCic.term DisambiguateTypes.codomain_item) list *
   NCic.metasenv *                  (* new metasenv *)
   NCic.substitution *
   NCic.term) list *  (* disambiguated term *)
  bool