diff options
| author | herbelin | 2000-12-14 22:13:07 +0000 |
|---|---|---|
| committer | herbelin | 2000-12-14 22:13:07 +0000 |
| commit | 42679bb4f94de0a25d6fe5a959e00cfe7a1454d9 (patch) | |
| tree | 02bca1d940eb146b99298a5ed9182122f73160e0 /scripts/coqc.ml | |
| parent | 32db56471909ae183832989670a81bf59b8a8e5c (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@1110 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts/coqc.ml')
0 files changed, 0 insertions, 0 deletions