diff options
| author | bgregoir | 2006-12-11 18:46:35 +0000 |
|---|---|---|
| committer | bgregoir | 2006-12-11 18:46:35 +0000 |
| commit | c86d78c0f18fb28f74bb6b192c03ebe73117cf03 (patch) | |
| tree | 99294164215016607e4056e5730a2d6c91043dbf /Makefile | |
| parent | 70c88a5f6d7e1ef184d70512969a6221eec8d11e (diff) | |
Changement dans le kernel :
- essai de suppression des dependances debiles. (echec)
- Application des patch debian.
Pour ring et field :
- introduciton de la function de sign et de puissance.
- Correction de certains bug.
- supression de ring_replace ....
Pour exact_no_check :
- ajout de la tactic : vm_cast_no_check (t)
qui remplace "exact_no_check (t<: type of Goal)"
(cette version forcais l'evaluation du cast dans le
pretypage).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9427 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 7 |
1 files changed, 3 insertions, 4 deletions
@@ -225,7 +225,7 @@ ML4FILES +=\ contrib/omega/g_omega.ml4 \ contrib/romega/g_romega.ml4 contrib/ring/g_quote.ml4 \ contrib/ring/g_ring.ml4 contrib/dp/g_dp.ml4 \ - contrib/setoid_ring/newring.ml4 \ + contrib/setoid_ring/newring.ml4 \ contrib/field/field.ml4 contrib/fourier/g_fourier.ml4 \ contrib/extraction/g_extraction.ml4 contrib/xml/xmlentries.ml4 @@ -874,7 +874,8 @@ ZARITHVO=\ theories/ZArith/Zdiv.vo theories/ZArith/Zsqrt.vo \ theories/ZArith/Zwf.vo theories/ZArith/ZArith_base.vo \ theories/ZArith/Zbool.vo theories/ZArith/Zbinary.vo \ - theories/ZArith/Znumtheory.vo theories/ZArith/Int.vo + theories/ZArith/Znumtheory.vo theories/ZArith/Int.vo \ + theories/ZArith/Zpow_def.vo QARITHVO=\ theories/QArith/QArith_base.vo theories/QArith/Qreduction.vo \ @@ -1754,8 +1755,6 @@ depend: beforedepend dependp4 ml4filesml done # 5. We express dependencies of .o files $(CC) -MM $(CINCLUDES) kernel/byterun/*.c >> .depend - $(CC) -MM $(CINCLUDES) kernel/byterun/*.c | sed -e 's/\.o/.d.o/' >> \ - .depend # 6. Finally, we erase the generated .ml files rm -f $(ML4FILESML) # 7. Since .depend contains correct dependencies .depend.devel can be deleted |