diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-31 21:56:37 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-31 21:56:37 +0000 |
| commit | 1d12b302120fbde8cbd7f8a3c36bf144a3e1e531 (patch) | |
| tree | 87d8f132c6872d3206f072ac0b16c051113f5d2c /Makefile | |
| parent | 6ca6bef6e701703ce38b89b81c89a61b2db3cb47 (diff) | |
ajout de QArith dans les theories standards
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8883 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 12 |
1 files changed, 9 insertions, 3 deletions
@@ -869,6 +869,11 @@ ZARITHVO=\ theories/ZArith/Zbool.vo theories/ZArith/Zbinary.vo \ theories/ZArith/Znumtheory.vo +QARITHVO=\ + theories/QArith/QArith_base.vo theories/QArith/Qreduction.vo \ + theories/QArith/Qring.vo theories/QArith/Qreals.vo \ + theories/QArith/QArith.vo + LISTSVO=\ theories/Lists/MonoList.vo \ theories/Lists/ListSet.vo theories/Lists/Streams.vo \ @@ -989,7 +994,7 @@ SETOIDSVO=theories/Setoids/Setoid.vo THEORIESVO =\ $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \ $(SETOIDSVO) $(LISTSVO) $(STRINGSVO) $(SETSVO) $(FSETSVO) $(INTMAPVO) \ - $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO) $(SORTINGVO) + $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO) $(SORTINGVO) $(QARITHVO) THEORIESLIGHTVO = $(INITVO) $(LOGICVO) $(ARITHVO) @@ -1001,6 +1006,7 @@ arith: $(ARITHVO) bool: $(BOOLVO) narith: $(NARITHVO) zarith: $(ZARITHVO) +qarith: $(QARITHVO) lists: $(LISTSVO) strings: $(STRINGSVO) sets: $(SETSVO) @@ -1015,8 +1021,8 @@ allreals: $(ALLREALS) setoids: $(SETOIDSVO) sorting: $(SORTINGVO) -noreal: logic arith bool zarith lists sets fsets intmap relations wellfounded \ - setoids sorting +noreal: logic arith bool zarith qarith lists sets fsets intmap relations \ + wellfounded setoids sorting ########################################################################### # contribs (interface not included) |