]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5b6965f) | patch
- metasenv is now checked
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 28 Oct 2002 12:34:38 +0000 (12:34 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 28 Oct 2002 12:34:38 +0000 (12:34 +0000)
commit125a10b86b9caf857e49867e2c0d8b101e0b3752
treed5e058ef70bccad5429a3e86ffd5cc32497dbb4dtree | snapshot
parent5b6965fc326021ec30894846113665d1b01fe8eecommit | diff
- metasenv is now checked
- the last commit introduced a bug: the debrujin function was called on
  the type of a constructor _before_ removing the left parameters. Fixed.
helm/ocaml/cic_proof_checking/cicTypeChecker.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.