diff options
| author | herbelin | 2004-02-03 17:34:35 +0000 |
|---|---|---|
| committer | herbelin | 2004-02-03 17:34:35 +0000 |
| commit | 8dc0a335e0b599e62f337ae0de999f3c673432c7 (patch) | |
| tree | 9b3b5542003a5bd22343f6a01a41fc43cf42ef2e /dev/base_db | |
| parent | ad6aa3994f75a94580bcea1bb77c5b6808bd5e39 (diff) | |
Relachement condition pour declarer un inductif dans la table des 'If'; contrainte de non dependances en les args des constructeurs pour avoir un affichage spontane avec if-then-else
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5284 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/base_db')
0 files changed, 0 insertions, 0 deletions