]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d5e420b) | patch
1) Implemented inference of the outtype for empty inductive types
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 7 Jun 2005 15:51:43 +0000 (15:51 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 7 Jun 2005 15:51:43 +0000 (15:51 +0000)
commit3c0cdcf6d775bfd19ed68f953d13773d2fb44772
tree0c4b81a8268b9299d7c6194747c35ab7900a40fbtree | snapshot
parentd5e420ba0286d6b6ccab7101bdd75a1442385e06commit | diff
1) Implemented inference of the outtype for empty inductive types
2) The inferred outtype (of non empty ind types) used to omit the lambda abstraction (worked using an amazing feature ot the type checker meant for backward compatibility with Coq 7... ask Claudio).
helm/ocaml/cic_unification/cicRefine.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.