diff options
| author | pottier | 2011-02-22 14:00:38 +0000 |
|---|---|---|
| committer | pottier | 2011-02-22 14:00:38 +0000 |
| commit | 4a2bd45d6b3c2adc90ac547f5afc0ebdd51c3293 (patch) | |
| tree | d0f2a0bc34454b9dfdf9b7fcb969ec08366cd701 /Makefile.common | |
| parent | 81dd7a1db170d7d10d8a378cfd0719c2ded3f7df (diff) | |
syntax for exponents
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13849 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/Makefile.common b/Makefile.common index fa76dac60b..a564d0e6a1 100644 --- a/Makefile.common +++ b/Makefile.common @@ -171,6 +171,7 @@ MICROMEGACMA:=plugins/micromega/micromega_plugin.cma QUOTECMA:=plugins/quote/quote_plugin.cma RINGCMA:=plugins/ring/ring_plugin.cma NEWRINGCMA:=plugins/setoid_ring/newring_plugin.cma +NCRINGCMA:=plugins/setoid_ring/ncring_plugin.cma NSATZCMA:=plugins/nsatz/nsatz_plugin.cma DPCMA:=plugins/dp/dp_plugin.cma FIELDCMA:=plugins/field/field_plugin.cma @@ -192,7 +193,7 @@ OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \ DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \ - $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(DPCMA) $(FIELDCMA) \ + $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(NCRINGCMA)$(DPCMA) $(FIELDCMA) \ $(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \ $(CCCMA) $(FOCMA) $(SUBTACCMA) $(RTAUTOCMA) \ $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA) @@ -305,6 +306,7 @@ QUOTEVO:=$(call cat_vo_itarget, plugins/quote) RINGVO:=$(call cat_vo_itarget, plugins/ring) FIELDVO:=$(call cat_vo_itarget, plugins/field) NEWRINGVO:=$(call cat_vo_itarget, plugins/setoid_ring) +NCRINGVO:=$(call cat_vo_itarget, plugins/setoid_ring) NSATZVO:=$(call cat_vo_itarget, plugins/nsatz) FOURIERVO:=$(call cat_vo_itarget, plugins/fourier) FUNINDVO:=$(call cat_vo_itarget, plugins/funind) @@ -316,7 +318,7 @@ CCVO:= PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \ $(XMLVO) $(FOURIERVO) $(CCVO) $(FUNINDVO) \ - $(RTAUTOVO) $(NEWRINGVO) $(DPVO) $(QUOTEVO) \ + $(RTAUTOVO) $(NEWRINGVO) $(NCRINGVO)$(DPVO) $(QUOTEVO) \ $(NSATZVO) $(EXTRACTIONVO) ALLVO:= $(THEORIESVO) $(PLUGINSVO) |