diff options
| author | Emilio Jesus Gallego Arias | 2020-03-14 23:14:12 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-30 19:05:37 -0400 |
| commit | 7b2e166eae2d9f83bf0e14f68075b0be0a8bd668 (patch) | |
| tree | 7b2a1bc0df009c41000c3a9c3a90fa1c6fa675db /vernac/classes.ml | |
| parent | 8fbc927ac40cc707b1a940d8339a2a289755d533 (diff) | |
[classes] Declare obligation implicits using standard API.
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index a882f6db0a..40c1a5d97d 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -334,10 +334,9 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst Impargs.maybe_declare_manual_implicits false cst impargs; instance_hook pri global cst -let declare_instance_program env sigma ~global ~poly name pri imps udecl term termtype = +let declare_instance_program env sigma ~global ~poly name pri impargs udecl term termtype = let hook { DeclareDef.Hook.S.scope; dref; _ } = let cst = match dref with GlobRef.ConstRef kn -> kn | _ -> assert false in - Impargs.declare_manual_implicits false dref imps; let pri = intern_info pri in let env = Global.env () in let sigma = Evd.from_env env in @@ -348,7 +347,7 @@ let declare_instance_program env sigma ~global ~poly name pri imps udecl term te let uctx = Evd.evar_universe_context sigma in let scope, kind = DeclareDef.Global Declare.ImportDefaultBehavior, Decls.Instance in let _ : DeclareObl.progress = - Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook typ ~uctx obls + Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls in () let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl ids term termtype = |