diff options
| author | Gaëtan Gilbert | 2019-02-22 15:56:05 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-22 15:56:05 +0100 |
| commit | 237050870a27bc2eda9224e9d8b18b7ef5b66236 (patch) | |
| tree | 14d07a9c21c2a97cd9289f0ecfae48c5e3d5bd6a /vernac/classes.ml | |
| parent | 7b282a5d041147a54b4553fe27db5c4c03c3e0f5 (diff) | |
| parent | 735d3fd21c65688143541d77c4153f52b963f4c4 (diff) | |
Merge PR #9314: Enrich implicits for instances
Reviewed-by: SkySkimmer
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 27d8b7390d..39c086eff5 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -106,7 +106,7 @@ let id_of_class cl = | _ -> assert false let instance_hook k info global imps ?hook cst = - Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps; + Impargs.maybe_declare_manual_implicits false cst imps; let info = intern_info info in Typeclasses.declare_instance (Some info) (not global) cst; (match hook with Some h -> h cst | None -> ()) @@ -149,7 +149,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id if program_mode then let hook _ _ vis gr = let cst = match gr with ConstRef kn -> kn | _ -> assert false in - Impargs.declare_manual_implicits false gr ~enriching:false [imps]; + Impargs.declare_manual_implicits false gr [imps]; let pri = intern_info pri in Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst) in |