diff options
Diffstat (limited to 'tactics/rewrite.ml4')
| -rw-r--r-- | tactics/rewrite.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index a6a36672b..9e017bbd8 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1410,7 +1410,7 @@ let add_morphism_infer glob m n = let instance = build_morphism_signature m in if Lib.is_modtype () then let cst = Declare.declare_constant ~internal:Declare.KernelSilent instance_id - (Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical) + (Entries.ParameterEntry (instance,None), Decl_kinds.IsAssumption Decl_kinds.Logical) in add_instance (Typeclasses.new_instance (Lazy.force proper_class) None glob (ConstRef cst)); declare_projection n instance_id (ConstRef cst) |