diff options
| author | herbelin | 2000-10-23 16:47:31 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-23 16:47:31 +0000 |
| commit | b87b4436461990fe0192b9897d252df9eaf6fc21 (patch) | |
| tree | 92893070688521340e499e7e0e23b52d53687463 /kernel/inductive.ml | |
| parent | 4f6b4c911f355b35c2b9a940cf78eb0cd21e4c12 (diff) | |
L'état implicite des définitions survivant au discharge redevient celui du moment de la définition (et non celui du moment de la fermeture de section) mais les args imps sont recalculés
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@740 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/inductive.ml')
0 files changed, 0 insertions, 0 deletions