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