diff options
| author | herbelin | 2008-06-01 20:18:52 +0000 |
|---|---|---|
| committer | herbelin | 2008-06-01 20:18:52 +0000 |
| commit | 026930883cfe2e1a431cc0259ed7f2cf2767c201 (patch) | |
| tree | 7b87294e26af25e5ddf433bd830210099ad9da45 /kernel/typeops.ml | |
| parent | 5e3a747ec4351a6cb07ac307196bad782bca1623 (diff) | |
On cesse de demander une valeur pour l'option reals si l'utilisateur
n'en donne pas (ça paraît plus simple vu que le temps de compil de
reals est devenu mineur, et on fait comme pour fsets qui par défaut
est compilé).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11031 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/typeops.ml')
0 files changed, 0 insertions, 0 deletions