diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-16 15:51:02 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-16 15:51:02 +0000 |
| commit | c5d686f2abee4f7d6376cfbdbc2d49c42c423c17 (patch) | |
| tree | d1d40416131888f1d8110225f817486dda537ad9 /.depend.coq | |
| parent | a6ef81988e1e4282cb2b7d6bf9a99576e032800d (diff) | |
Nouveau mécanisme pour les modules interactifs : les arguments de
foncteurs sont données un par un ce qui permet de faire les
load_objects correspondants au bon moment (càd juste après l'ajout des
déclarations logiques et avant l'ajout du paramètre suivant). Ceci
clôt le bug #1118 et corrige des erreurs de localisation introduite
par le commit précédent.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8723 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to '.depend.coq')
0 files changed, 0 insertions, 0 deletions