Merge PR #13183: attribute #[using] for Definition and Fixpoint

Reviewed-by: SkySkimmer
Ack-by: herbelin
Ack-by: Zimmi48

1 files changed, 14 insertions, 4 deletions

diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index c1dbf0a1ea..3fc74cba5b 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -110,7 +110,7 @@ let interp_definition ~program_mode env evd impl_env bl red_option c ctypopt =
   let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in
   evd, (c, tyopt), imps
 
-let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
+let do_definition ?hook ~name ~scope ~poly ~kind ?using udecl bl red_option c ctypopt =
   let program_mode = false in
   let env = Global.env() in
   (* Explicitly bound universes and constraints *)
@@ -118,14 +118,19 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
   let evd, (body, types), impargs =
     interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt
   in
+  let using = using |> Option.map (fun expr ->
+    let terms = body :: match types with Some x -> [x] | None -> [] in
+    let l = Proof_using.process_expr (Global.env()) evd expr terms in
+    Names.Id.Set.(List.fold_right add l empty))
+  in
   let kind = Decls.IsDefinition kind in
-  let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in
+  let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types ?using () in
   let info = Declare.Info.make ~scope ~kind ?hook ~udecl ~poly () in
   let _ : Names.GlobRef.t =
     Declare.declare_definition ~info ~cinfo ~opaque:false ~body evd
   in ()
 
-let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
+let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind ?using udecl bl red_option c ctypopt =
   let program_mode = true in
   let env = Global.env() in
   (* Explicitly bound universes and constraints *)
@@ -133,9 +138,14 @@ let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind udecl bl red_option
   let evd, (body, types), impargs =
     interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt
   in
+  let using = using |> Option.map (fun expr ->
+    let terms = body :: match types with Some x -> [x] | None -> [] in
+    let l = Proof_using.process_expr (Global.env()) evd expr terms in
+    Names.Id.Set.(List.fold_right add l empty))
+  in
   let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in
   let pm, _ =
-    let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
+    let cinfo = Declare.CInfo.make ~name ~typ ~impargs ?using () in
     let info = Declare.Info.make ~udecl ~scope ~poly ~kind ?hook () in
     Declare.Obls.add_definition ~pm ~cinfo ~info ~term ~uctx obls
   in pm