From 39e45f296afefc936e3a63836d7f56c482ddee7a Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 12 Oct 2020 11:16:20 +0200
Subject: attribute #[using] for Definition and Fixpoint

---
 vernac/comFixpoint.ml | 22 ++++++++++++++--------
 1 file changed, 14 insertions(+), 8 deletions(-)

(limited to 'vernac/comFixpoint.ml')

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 78572c6aa6..bd11fa2b47 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -251,15 +251,21 @@ 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 +283,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 +334,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 +348,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
-- 
cgit v1.2.3


From 7de7fe612ffc5a598311f9542e57e50803ff2007 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 13 Oct 2020 15:32:54 +0200
Subject: [doc] attribute #[using]

---
 vernac/comFixpoint.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'vernac/comFixpoint.ml')

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index bd11fa2b47..29bf5fbcc2 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -263,7 +263,8 @@ let build_recthms ~indexes ?using fixnames fixtypes fiximps =
           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
+          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 ?using ()
       ) fixnames fixtypes fiximps
-- 
cgit v1.2.3