]> matita.cs.unibo.it Git - helm.git/commit
- number notation ported to new library
authorAndrea Asperti <andrea.asperti@unibo.it>
Thu, 18 Nov 2010 10:44:56 +0000 (10:44 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Thu, 18 Nov 2010 10:44:56 +0000 (10:44 +0000)
commit4556677f40e6b979d9bdaa4475bb1ca6701264f8
tree49293c0511b33069658966197330dcbf8be98d2f
parent09c63c35520ceea6f0caaa0be856a3eaff46bb88
- number notation ported to new library
- code for number notation made less general by hard-coding the only
  notation
matita/components/ng_disambiguation/.depend
matita/components/ng_disambiguation/Makefile
matita/components/ng_disambiguation/disambiguateChoices.ml
matita/components/ng_disambiguation/disambiguateChoices.mli
matita/components/ng_disambiguation/grafiteDisambiguate.ml
matita/components/ng_disambiguation/nnumber_notation.ml
matita/components/ng_disambiguation/nnumber_notation.mli