]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f5916a7) | patch
Less verbose error messages (= substitution applied everywhere, terms pretty
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 19 Nov 2005 17:51:54 +0000 (17:51 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 19 Nov 2005 17:51:54 +0000 (17:51 +0000)
commit5c3ae2f17d55098676bd50270ddef0bec93618bf
treeec032117dd014a4c6fa04055e21f50832110bd61tree | snapshot
parentf5916a7ca7e58c6a3617531e8dbba81d018eb024commit | diff
Less verbose error messages (= substitution applied everywhere, terms pretty
printed in their context) are now printed by default.
There is a flag in cicUnification.ml to set the error messages to the
verbose mode.
helm/ocaml/cic_disambiguation/disambiguate.ml diff | blob | history
helm/ocaml/cic_unification/cicMetaSubst.ml diff | blob | history
helm/ocaml/cic_unification/cicMetaSubst.mli diff | blob | history
helm/ocaml/cic_unification/cicUnification.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.