]> matita.cs.unibo.it Git - helm.git/commit
- Disambiguation error exception enriched with more information
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 18 Oct 2006 15:06:03 +0000 (15:06 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 18 Oct 2006 15:06:03 +0000 (15:06 +0000)
commit6809084b2a99a1a7e64d87ca939118f77c07b8b5
tree6dd059626d3edaadce2c00e30394d4e46608362f
parent79f497094d49963fe9f335e00b58aecc79cbc461
- Disambiguation error exception enriched with more information
  (the same returned in case of correct disambiguation)
- The disambiguation error interface now shows the complete environment
  in which the error occurs. I am not sure if this is better or worst than
  showing only the diffs.
helm/software/components/cic_disambiguation/disambiguate.ml
helm/software/components/cic_disambiguation/disambiguate.mli
helm/software/components/grafite_parser/grafiteDisambiguate.ml
helm/software/components/grafite_parser/grafiteDisambiguator.ml
helm/software/components/grafite_parser/grafiteDisambiguator.mli
helm/software/matita/matitaExcPp.ml
helm/software/matita/matitaGui.ml