Merge PR #10316: [lemmas] Reify info for implicits, universe decls, and rec theorems.

Reviewed-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: ppedrot

1 files changed, 12 insertions, 12 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index d6a2f2727a..8addfa054e 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -362,21 +362,21 @@ let declare_instance_program env sigma ~global ~poly id pri imps decl term termt
   in
   let hook = DeclareDef.Hook.make hook in
   let ctx = Evd.evar_universe_context sigma in
-  ignore(Obligations.add_definition id ?term:constr
-           ~univdecl:decl typ ctx ~kind:(Global ImportDefaultBehavior,poly,Instance) ~hook obls)
+  ignore(Obligations.add_definition ~name:id ?term:constr
+           ~univdecl:decl ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly ~kind:Instance ~hook typ ctx obls)
 
-
-let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids term termtype =
+let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids term termtype =
   (* spiwack: it is hard to reorder the actions to do
      the pretyping after the proof has opened. As a
      consequence, we use the low-level primitives to code
      the refinement manually.*)
   let gls = List.rev (Evd.future_goals sigma) in
   let sigma = Evd.reset_future_goals sigma in
-  let kind = Decl_kinds.(Global ImportDefaultBehavior, poly, DefinitionBody Instance) in
-  let lemma = Lemmas.start_lemma id ~pl:decl kind sigma (EConstr.of_constr termtype)
-      ~hook:(DeclareDef.Hook.make
-               (fun _ _ _ -> instance_hook pri global imps ?hook)) in
+  let scope = DeclareDef.Global Declare.ImportDefaultBehavior in
+  let kind = Decl_kinds.DefinitionBody Decl_kinds.Instance in
+  let hook = DeclareDef.Hook.make (fun _ _ _ -> instance_hook pri global imps ?hook) in
+  let info = Lemmas.Info.make ~hook ~scope ~kind () in
+  let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info sigma (EConstr.of_constr termtype) in
   (* spiwack: I don't know what to do with the status here. *)
   let lemma =
     if not (Option.is_empty term) then
@@ -567,7 +567,7 @@ let new_instance_common ~program_mode ~generalize env instid ctx cl =
   id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl
 
 let new_instance_interactive ?(global=false)
-    poly instid ctx cl
+    ~poly instid ctx cl
     ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
   let env = Global.env() in
   let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
@@ -576,7 +576,7 @@ let new_instance_interactive ?(global=false)
     cty k u ctx ctx' pri decl imps subst id
 
 let new_instance_program ?(global=false)
-    poly instid ctx cl opt_props
+    ~poly instid ctx cl opt_props
     ?(generalize=true) ?hook pri =
   let env = Global.env() in
   let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
@@ -586,7 +586,7 @@ let new_instance_program ?(global=false)
   id
 
 let new_instance ?(global=false)
-    poly instid ctx cl props
+    ~poly instid ctx cl props
     ?(generalize=true) ?hook pri =
   let env = Global.env() in
   let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
@@ -595,7 +595,7 @@ let new_instance ?(global=false)
     cty k u ctx ctx' pri decl imps subst id props;
   id
 
-let declare_new_instance ?(global=false) ~program_mode poly instid ctx cl pri =
+let declare_new_instance ?(global=false) ~program_mode ~poly instid ctx cl pri =
   let env = Global.env() in
   let ({CAst.loc;v=instid}, pl) = instid in
   let sigma, k, u, cty, ctx', ctx, imps, subst, decl =