]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a335fa8) | patch
Defs in context may now have an optional type (when unknown).
authorStefano Zacchiroli <zack@upsilon.cc>
Fri, 5 Sep 2003 16:23:17 +0000 (16:23 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Fri, 5 Sep 2003 16:23:17 +0000 (16:23 +0000)
commite1d3db51fb0d63c882c0a40d9b91bc28ab05747e
treeee08eb787a91e306222eace05dfddd672a5d9515tree | snapshot
parenta335fa89b0340ba3fb5d60566075ca83b5bda5d1commit | diff
Defs in context may now have an optional type (when unknown).

During type-checking, LetIn are pushed in the context as Defs with a known
type. When a Rel pointing to a Def in the context is found, the already
computed type (if present) is used instead of re-typing the body of the
LetIn. As a result, we get a (possibly exponential) decrease in the complexity
of the typing algorithm.
helm/ocaml/cic_omdoc/content2cic.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.