diff options
Diffstat (limited to 'plugins/subtac/subtac_command.ml')
| -rw-r--r-- | plugins/subtac/subtac_command.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index 5c7f7b5ec0..f02e83ad1a 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -327,7 +327,6 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = let ce = { const_entry_body = Evarutil.nf_evar !isevars body; const_entry_type = Some ty; - const_entry_polymorphic = false; const_entry_opaque = false } in let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in |