diff options
| author | sacerdot | 2004-07-08 15:24:51 +0000 |
|---|---|---|
| committer | sacerdot | 2004-07-08 15:24:51 +0000 |
| commit | 4b391cb815064a6ad5f5413c0e4054c6e4f4bd8a (patch) | |
| tree | d8238260a36986a2182c9f689cec982b87e3a3df /kernel | |
| parent | f8eef6662a92d8bb739da9a0fe1227a9fd111b4b (diff) | |
- recent changes to doubleTypeInference.ml (that introduced double
type inference for inferred types) undone. Previous performance restored.
- bug in cic2acic (code that used to be dead fixed): the type of a sort
was computed as the sort itself
- CPropRetyping in cic2acic modified to handle correctly the sort Set in
the two cases Predicative Set / Impredicative Set
- CPropRetyping.get_type_of used in place of Retyping.get_type_of everywhere
in cic2acic. This closes (again, but more efficiently) the bug about
CProps erroneously recognized as Types in inferred types
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5875 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions