attribute #[using] for Definition and Fixpoint

1 files changed, 18 insertions, 10 deletions

diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 55901fd604..c2e07c4fd5 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -109,7 +109,7 @@ let telescope env sigma l =
 let nf_evar_context sigma ctx =
   List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx
 
-let build_wellfounded pm (recname,pl,bl,arityc,body) poly r measure notation =
+let build_wellfounded pm (recname,pl,bl,arityc,body) poly ?using r measure notation =
   let open EConstr in
   let open Vars in
   let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
@@ -259,8 +259,12 @@ let build_wellfounded pm (recname,pl,bl,arityc,body) poly r measure notation =
   let evars, _, evars_def, evars_typ =
     RetrieveObl.retrieve_obligations env recname sigma 0 def typ
   in
+  let using = using |> Option.map (fun expr ->
+    let terms = List.map EConstr.of_constr [evars_def; evars_typ] in
+    let l = Proof_using.process_expr env sigma expr terms in
+    Names.Id.Set.(List.fold_right add l empty)) in
   let uctx = Evd.evar_universe_context sigma in
-  let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ () in
+  let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ ?using () in
   let info = Declare.Info.make ~udecl ~poly ~hook () in
   let pm, _ =
     Declare.Obls.add_definition ~pm ~cinfo ~info ~term:evars_def ~uctx evars in
@@ -275,7 +279,7 @@ let collect_evars_of_term evd c ty =
   Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
   evars (Evd.from_ctx (Evd.evar_universe_context evd))
 
-let do_program_recursive ~pm ~scope ~poly fixkind fixl =
+let do_program_recursive ~pm ~scope ~poly ?using fixkind fixl =
   let cofix = fixkind = Declare.Obls.IsCoFixpoint in
   let (env, rec_sign, udecl, evd), fix, info =
     interp_recursive ~cofix ~program_mode:true fixl
@@ -287,13 +291,17 @@ let do_program_recursive ~pm ~scope ~poly fixkind fixl =
   let evd = nf_evar_map_undefined evd in
   let collect_evars name def typ impargs =
     (* Generalize by the recursive prototypes  *)
+    let using = using |> Option.map (fun expr ->
+      let terms = [def; typ] in
+      let l = Proof_using.process_expr env evd expr terms in
+      Names.Id.Set.(List.fold_right add l empty)) in
     let def = nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) in
     let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in
     let evm = collect_evars_of_term evd def typ in
     let evars, _, def, typ =
       RetrieveObl.retrieve_obligations env name evm
         (List.length rec_sign) def typ in
-    let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
+    let cinfo = Declare.CInfo.make ~name ~typ ~impargs ?using () in
     (cinfo, def, evars)
   in
   let (fixnames,fixrs,fixdefs,fixtypes) = fix in
@@ -325,13 +333,13 @@ let do_program_recursive ~pm ~scope ~poly fixkind fixl =
   let info = Declare.Info.make ~poly ~scope ~kind ~udecl () in
   Declare.Obls.add_mutual_definitions ~pm defs ~info ~uctx ~ntns fixkind
 
-let do_fixpoint ~pm ~scope ~poly l =
+let do_fixpoint ~pm ~scope ~poly ?using l =
   let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in
     match g, l with
     | [Some { CAst.v = CWfRec (n,r) }],
       [ Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations} ] ->
         let recarg = mkIdentC n.CAst.v in
-        build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly r recarg notations
+        build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly ?using r recarg notations
 
     | [Some { CAst.v = CMeasureRec (n, m, r) }],
       [Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations }] ->
@@ -344,7 +352,7 @@ let do_fixpoint ~pm ~scope ~poly l =
           user_err Pp.(str"Measure takes only two arguments in Program Fixpoint.")
         | _, _ -> r
       in
-        build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly
+        build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly ?using
           (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m notations
 
     | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g ->
@@ -352,11 +360,11 @@ let do_fixpoint ~pm ~scope ~poly l =
           Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in
       let fixkind = Declare.Obls.IsFixpoint annots in
       let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in
-      do_program_recursive ~pm ~scope ~poly fixkind l
+      do_program_recursive ~pm ~scope ~poly ?using fixkind l
     | _, _ ->
       CErrors.user_err ~hdr:"do_fixpoint"
         (str "Well-founded fixpoints not allowed in mutually recursive blocks")
 
-let do_cofixpoint ~pm ~scope ~poly fixl =
+let do_cofixpoint ~pm ~scope ~poly ?using fixl =
   let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in
-  do_program_recursive ~pm ~scope ~poly Declare.Obls.IsCoFixpoint fixl
+  do_program_recursive ~pm ~scope ~poly ?using Declare.Obls.IsCoFixpoint fixl