]> matita.cs.unibo.it Git - helm.git/commit
Disambiguation errors are no longer thrown away. They are now collected
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 19 Nov 2005 15:02:08 +0000 (15:02 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 19 Nov 2005 15:02:08 +0000 (15:02 +0000)
commit2bb6c98121db82a1c67565bb528787f2def7192d
tree0cb6d45860ab1f9589e4f10f9c453f857441de52
parent192884dae520029b152a3f69989e51cc8af158ce
Disambiguation errors are no longer thrown away. They are now collected
and presented (in a not understandable way) to the user.
12 files changed:
helm/matita/.depend
helm/matita/Makefile.in
helm/matita/matitaDisambiguator.ml
helm/matita/matitaDisambiguator.mli
helm/matita/matitaEngine.ml
helm/matita/matitaExcPp.ml
helm/ocaml/cic_disambiguation/disambiguate.ml
helm/ocaml/cic_disambiguation/disambiguate.mli
helm/ocaml/cic_disambiguation/disambiguateChoices.ml
helm/ocaml/cic_disambiguation/disambiguateTypes.ml
helm/ocaml/cic_disambiguation/disambiguateTypes.mli
helm/ocaml/cic_disambiguation/number_notation.ml