]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: dc8d0fc) | patch
~subst fixed everywhere in the type-checker:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 25 Oct 2005 11:11:40 +0000 (11:11 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 25 Oct 2005 11:11:40 +0000 (11:11 +0000)
commite174574339e22f1d6a518f9b272ad412a0cd7a90
treed3152703b88125bac1d762393f413944ee93aa8ftree | snapshot
parentdc8d0fc140ba531d2f0bad60b9be2991f7a6475bcommit | diff
~subst fixed everywhere in the type-checker:
 1. sometimes it was not passed to functions
 2. sometimes it was passed but it was not used/useful/correct
 3. sometimes it was not passed recursively
helm/ocaml/cic_proof_checking/cicTypeChecker.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.