]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: db3104b) | patch
Even if the error is not localized, it was not a good idea to make the unification...
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 4 Dec 2007 22:01:38 +0000 (22:01 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 4 Dec 2007 22:01:38 +0000 (22:01 +0000)
commitb89690596acb0b24f1fd45da28ac04b4ad217e98
tree02f33d4be5615a4031b05f05eb817bb18b861c6dtree | snapshot
parentdb3104b6a36b957d7be4c79e50f22fd0ffd90f0dcommit | diff
Even if the error is not localized, it was not a good idea to make the unification error
escape.
helm/software/components/cic_unification/cicRefine.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.