aboutsummaryrefslogtreecommitdiff
path: root/plugins/pluginsopt.itarget
diff options
context:
space:
mode:
authorpottier2011-02-22 14:00:38 +0000
committerpottier2011-02-22 14:00:38 +0000
commit4a2bd45d6b3c2adc90ac547f5afc0ebdd51c3293 (patch)
treed0f2a0bc34454b9dfdf9b7fcb969ec08366cd701 /plugins/pluginsopt.itarget
parent81dd7a1db170d7d10d8a378cfd0719c2ded3f7df (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 'plugins/pluginsopt.itarget')
-rw-r--r--plugins/pluginsopt.itarget1
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/pluginsopt.itarget b/plugins/pluginsopt.itarget
index 74b3f5275f..84ba2c6d74 100644
--- a/plugins/pluginsopt.itarget
+++ b/plugins/pluginsopt.itarget
@@ -13,6 +13,7 @@ xml/xml_plugin.cmxa
subtac/subtac_plugin.cmxa
ring/ring_plugin.cmxa
cc/cc_plugin.cmxa
+ncring/ncring_plugin.cmxa
nsatz/nsatz_plugin.cmxa
funind/recdef_plugin.cmxa
syntax/ascii_syntax_plugin.cmxa