]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 358cefe) | patch
Refinement of CurrentProof did not check whether the type is a type.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 15 Jun 2005 11:22:55 +0000 (11:22 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 15 Jun 2005 11:22:55 +0000 (11:22 +0000)
commit4a3a4a798967ddea5c537ed09e91c7218a5f67b3
treeb8a1cff0fe9f6262c1a2db725f7d7fa47efc4caftree | snapshot
parent358cefe50cccd4cb7d8e2a9cecb7efcb5780b8a3commit | diff
Refinement of CurrentProof did not check whether the type is a type.
As a consequence it was possible to do "theorem t: 0" :-)
helm/ocaml/cic_unification/cicRefine.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.