diff options
| author | herbelin | 2000-12-14 22:18:47 +0000 |
|---|---|---|
| committer | herbelin | 2000-12-14 22:18:47 +0000 |
| commit | ed20a4e9c320ae4bb2f724d181fbb351079d00b2 (patch) | |
| tree | f2c40c77ed55f6da9dff40c8b54e83a5afeaaf24 /dev/base_db | |
| parent | 910650274c33e28ba71ee8f1194ab9a6db69dfd7 (diff) | |
Les params d'inductif deviennent en même temps propre à chaque inductif d'un bloc et en même temps factorisés dans l'arité et les constructeurs (ceci est valable pour mutual_inductive_packet mais pas pour mutual_inductive_body); accessoirement cela permet de factoriser le calcul des univers des paramètres dans safe_typing
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1113 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/base_db')
0 files changed, 0 insertions, 0 deletions