diff options
| author | Pierre-Marie Pédrot | 2018-11-06 18:40:20 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-06 18:40:20 +0100 |
| commit | 92d1a0c14ef326929b6870541073bcae4d2c895d (patch) | |
| tree | 4e4e722b7d8881ad29d790a4a0dfd24a7e8a4226 /vernac/classes.ml | |
| parent | f6033667bd9b8069308d4bcba420c4ce0771e44f (diff) | |
| parent | 05336f66483eec4c34f19df937d28b8bdae8749a (diff) | |
Merge PR #8889: Program hook gives back an obligation substitiution
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 84ffb84206..f4b0015851 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -149,7 +149,7 @@ let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imp let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype = let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in if program_mode then - let hook _ vis gr = + let hook _ _ vis gr = let cst = match gr with ConstRef kn -> kn | _ -> assert false in Impargs.declare_manual_implicits false gr ~enriching:false [imps]; let pri = intern_info pri in |