diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-08-14 20:43:22 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-08-14 20:43:22 +0000 |
| commit | 7374c787f4a2bb0d50e2d9348e559b1c94dfff5b (patch) | |
| tree | 6d26b9e249bbb6d8c19a2879cc405a1553ccacb0 /Makefile | |
| parent | 4135e812a99fdfd7404fd354f31f286a4b4f005a (diff) | |
Fusion -translate et -ftranslate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4276 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 7 |
1 files changed, 4 insertions, 3 deletions
@@ -212,7 +212,8 @@ ML4FILES += contrib/interface/debug_tac.ml4 contrib/interface/centaur.ml4 PARSERREQUIRES=$(CMO) # Solution de facilité... PARSERREQUIRESCMX=$(PARSERREQUIRES:.cmo=.cmx) -ML4FILES += contrib/correctness/psyntax.ml4 contrib/omega/g_omega.ml4 \ +ML4FILES +=\ + contrib/correctness/psyntax.ml4 contrib/omega/g_omega.ml4 \ contrib/romega/g_romega.ml4 contrib/ring/g_quote.ml4 \ contrib/ring/g_ring.ml4 \ contrib/field/field.ml4 contrib/fourier/g_fourier.ml4 \ @@ -717,7 +718,7 @@ CORRECTNESSVO=contrib/correctness/Arrays.vo \ contrib/correctness/Exchange.vo \ contrib/correctness/ArrayPermut.vo \ contrib/correctness/ProgBool.vo contrib/correctness/ProgInt.vo \ - contrib/correctness/Sorted.vo contrib/correctness/Tuples.vo + contrib/correctness/Sorted.vo contrib/correctness/Tuples.vo # contrib/correctness/ProgramsExtraction.vo OMEGAVO = contrib/omega/Omega.vo @@ -1274,7 +1275,7 @@ devel: # 1. Translate the old syntax files and build new syntax theories hierarchy translation:: - @$(MAKE) COQ_XML="-ftranslate -no-strict" world + @$(MAKE) COQ_XML="-translate -no-strict" world @$(MAKE) movenew movenew:: |