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

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

1 files changed, 15 insertions, 8 deletions

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 78572c6aa6..29bf5fbcc2 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -251,15 +251,22 @@ let interp_fixpoint ?(check_recursivity=true) ~cofix l :
   let uctx,fix = ground_fixpoint env evd fix in
   (fix,pl,uctx,info)
 
-let build_recthms ~indexes fixnames fixtypes fiximps =
+let build_recthms ~indexes ?using fixnames fixtypes fiximps =
   let fix_kind, cofix = match indexes with
     | Some indexes -> Decls.Fixpoint, false
     | None -> Decls.CoFixpoint, true
   in
   let thms =
     List.map3 (fun name typ (ctx,impargs,_) ->
+        let using = using |> Option.map (fun expr ->
+          let terms = [EConstr.of_constr typ] in
+          let env = Global.env() in
+          let sigma = Evd.from_env env in
+          let l = Proof_using.process_expr env sigma expr terms in
+          Names.Id.Set.(List.fold_right add l empty))
+        in
         let args = List.map Context.Rel.Declaration.get_name ctx in
-        Declare.CInfo.make ~name ~typ ~args ~impargs ()
+        Declare.CInfo.make ~name ~typ ~args ~impargs ?using ()
       ) fixnames fixtypes fiximps
   in
   fix_kind, cofix, thms
@@ -277,9 +284,9 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   lemma
 
-let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns =
+let declare_fixpoint_generic ?indexes ~scope ~poly ?using ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns =
   (* We shortcut the proof process *)
-  let fix_kind, cofix, fixitems = build_recthms ~indexes fixnames fixtypes fiximps in
+  let fix_kind, cofix, fixitems = build_recthms ~indexes ?using fixnames fixtypes fiximps in
   let fixdefs = List.map Option.get fixdefs in
   let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
   let fix_kind = Decls.IsDefinition fix_kind in
@@ -328,9 +335,9 @@ let do_fixpoint_interactive ~scope ~poly l : Declare.Proof.t =
   let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ~poly fix ntns in
   lemma
 
-let do_fixpoint ~scope ~poly l =
+let do_fixpoint ~scope ~poly ?using l =
   let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in
-  declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly fix ntns
+  declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly ?using fix ntns
 
 let do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) =
   let fixl = List.map (fun fix -> {fix with Vernacexpr.rec_order = None}) fixl in
@@ -342,6 +349,6 @@ let do_cofixpoint_interactive ~scope ~poly l =
   let lemma = declare_fixpoint_interactive_generic ~scope ~poly cofix ntns in
   lemma
 
-let do_cofixpoint ~scope ~poly l =
+let do_cofixpoint ~scope ~poly ?using l =
   let cofix, ntns = do_cofixpoint_common l in
-  declare_fixpoint_generic ~scope ~poly cofix ntns
+  declare_fixpoint_generic ~scope ~poly ?using cofix ntns