aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/setoid_ring')
-rw-r--r--plugins/setoid_ring/newring.ml41
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 38c65cdd09..d434a890f1 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -159,6 +159,7 @@ let decl_constant na c =
mkConst(declare_constant (id_of_string na) (DefinitionEntry
{ const_entry_body = c;
const_entry_type = None;
+ const_entry_polymorphic = false;
const_entry_opaque = true },
IsProof Lemma))