attribute #[using] for Definition and Fixpoint

1 files changed, 52 insertions, 39 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 3ced38d6ea..b6e7d22732 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -57,14 +57,16 @@ module DefAttributes = struct
     program : bool;
     deprecated : Deprecation.t option;
     canonical_instance : bool;
+    using : Vernacexpr.section_subset_expr option;
   }
 
   let parse f =
     let open Attributes in
-    let (((locality, deprecated), polymorphic), program), canonical_instance =
-      parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance) f
+    let ((((locality, deprecated), polymorphic), program), canonical_instance), using =
+      parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance ++ using) f
     in
-    { polymorphic; program; locality; deprecated; canonical_instance }
+    let using = Option.map Proof_using.using_from_string using in
+    { polymorphic; program; locality; deprecated; canonical_instance; using }
 end
 
 let module_locality = Attributes.Notations.(locality >>= fun l -> return (make_module_locality l))
@@ -496,6 +498,25 @@ let program_inference_hook env sigma ev =
     user_err Pp.(str "The statement obligations could not be resolved \
                       automatically, write a statement definition first.")
 
+let vernac_set_used_variables ~pstate e : Declare.Proof.t =
+  let env = Global.env () in
+  let sigma, _ = Declare.Proof.get_current_context pstate in
+  let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in
+  let tys = List.map snd (initial_goals (Declare.Proof.get pstate)) in
+  let l = Proof_using.process_expr env sigma e tys in
+  let vars = Environ.named_context env in
+  List.iter (fun id ->
+    if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then
+      user_err ~hdr:"vernac_set_used_variables"
+        (str "Unknown variable: " ++ Id.print id))
+    l;
+  let _, pstate = Declare.Proof.set_used_variables pstate l in
+  pstate
+let vernac_set_used_variables_opt ?using pstate =
+  match using with
+  | None -> pstate
+  | Some expr -> vernac_set_used_variables ~pstate expr
+
 (* XXX: Interpretation of lemma command, duplication with ComFixpoint
    / ComDefinition ? *)
 let interp_lemma ~program_mode ~flags ~scope env0 evd thms =
@@ -525,7 +546,7 @@ let post_check_evd ~udecl ~poly evd =
   else (* We fix the variables to ensure they won't be lowered to Set *)
     Evd.fix_undefined_variables evd
 
-let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
+let start_lemma_com ~program_mode ~poly ~scope ~kind ?using ?hook thms =
   let env0 = Global.env () in
   let flags = Pretyping.{ all_no_fail_flags with program_mode } in
   let decl = fst (List.hd thms) in
@@ -533,17 +554,20 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
   let evd, thms = interp_lemma ~program_mode ~flags ~scope env0 evd thms in
   let mut_analysis = RecLemmas.look_for_possibly_mutual_statements evd thms in
   let evd = Evd.minimize_universes evd in
-  match mut_analysis with
-  | RecLemmas.NonMutual thm ->
-    let thm = Declare.CInfo.to_constr evd thm in
-    let evd = post_check_evd ~udecl ~poly evd in
-    let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in
-    Declare.Proof.start_with_initialization ~info ~cinfo:thm evd
-  | RecLemmas.Mutual { mutual_info; cinfo ; possible_guards } ->
-    let cinfo = List.map (Declare.CInfo.to_constr evd) cinfo in
-    let evd = post_check_evd ~udecl ~poly evd in
-    let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in
-    Declare.Proof.start_mutual_with_initialization ~info ~cinfo evd ~mutual_info (Some possible_guards)
+  let pstate =
+    match mut_analysis with
+    | RecLemmas.NonMutual thm ->
+      let thm = Declare.CInfo.to_constr evd thm in
+      let evd = post_check_evd ~udecl ~poly evd in
+      let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in
+      Declare.Proof.start_with_initialization ~info ~cinfo:thm evd
+    | RecLemmas.Mutual { mutual_info; cinfo ; possible_guards } ->
+      let cinfo = List.map (Declare.CInfo.to_constr evd) cinfo in
+      let evd = post_check_evd ~udecl ~poly evd in
+      let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in
+      Declare.Proof.start_mutual_with_initialization ~info ~cinfo evd ~mutual_info (Some possible_guards)
+  in
+  vernac_set_used_variables_opt ?using pstate
 
 let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function
 | Coercion ->
@@ -583,7 +607,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
   let program_mode = atts.program in
   let poly = atts.polymorphic in
   let name = vernac_definition_name lid local in
-  start_lemma_com ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?hook [(name, pl), (bl, t)]
+  start_lemma_com ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?using:atts.using ?hook [(name, pl), (bl, t)]
 
 let vernac_definition ~atts ~pm (discharge, kind) (lid, pl) bl red_option c typ_opt =
   let open DefAttributes in
@@ -604,7 +628,7 @@ let vernac_definition ~atts ~pm (discharge, kind) (lid, pl) bl red_option c typ_
   else
     let () =
       ComDefinition.do_definition ~name:name.v
-        ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook in
+        ~poly:atts.polymorphic ~scope ~kind ?using:atts.using pl bl red_option c typ_opt ?hook in
     pm
 
 (* NB: pstate argument to use combinators easily *)
@@ -613,7 +637,7 @@ let vernac_start_proof ~atts kind l =
   let scope = enforce_locality_exp atts.locality NoDischarge in
   if Dumpglob.dump () then
     List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
-  start_lemma_com ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.IsProof kind) l
+  start_lemma_com ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.IsProof kind) ?using:atts.using l
 
 let vernac_end_proof ~lemma ~pm = let open Vernacexpr in function
   | Admitted ->
@@ -639,6 +663,8 @@ let vernac_assumption ~atts discharge kind l nl =
           match scope with
             | Global _ -> Dumpglob.dump_definition lid false "ax"
             | Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
+  if Option.has_some atts.using then
+    Attributes.unsupported_attributes  ["using",VernacFlagEmpty];
   ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l
 
 let is_polymorphic_inductive_cumulativity =
@@ -842,16 +868,17 @@ let vernac_fixpoint_interactive ~atts discharge l =
   let scope = vernac_fixpoint_common ~atts discharge l in
   if atts.program then
     CErrors.user_err Pp.(str"Program Fixpoint requires a body");
-  ComFixpoint.do_fixpoint_interactive ~scope ~poly:atts.polymorphic l
+  vernac_set_used_variables_opt ?using:atts.using
+    (ComFixpoint.do_fixpoint_interactive ~scope ~poly:atts.polymorphic l)
 
 let vernac_fixpoint ~atts ~pm discharge l =
   let open DefAttributes in
   let scope = vernac_fixpoint_common ~atts discharge l in
   if atts.program then
     (* XXX: Switch to the attribute system and match on ~atts *)
-    ComProgramFixpoint.do_fixpoint ~pm ~scope ~poly:atts.polymorphic l
+    ComProgramFixpoint.do_fixpoint ~pm ~scope ~poly:atts.polymorphic ?using:atts.using l
   else
-    let () = ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic l in
+    let () = ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic ?using:atts.using l in
     pm
 
 let vernac_cofixpoint_common ~atts discharge l =
@@ -864,15 +891,16 @@ let vernac_cofixpoint_interactive ~atts discharge l =
   let scope = vernac_cofixpoint_common ~atts discharge l in
   if atts.program then
     CErrors.user_err Pp.(str"Program CoFixpoint requires a body");
-  ComFixpoint.do_cofixpoint_interactive ~scope ~poly:atts.polymorphic l
+  vernac_set_used_variables_opt ?using:atts.using
+    (ComFixpoint.do_cofixpoint_interactive ~scope ~poly:atts.polymorphic l)
 
 let vernac_cofixpoint ~atts ~pm discharge l =
   let open DefAttributes in
   let scope = vernac_cofixpoint_common ~atts discharge l in
   if atts.program then
-    ComProgramFixpoint.do_cofixpoint ~pm ~scope ~poly:atts.polymorphic l
+    ComProgramFixpoint.do_cofixpoint ~pm ~scope ~poly:atts.polymorphic ?using:atts.using l
   else
-    let () = ComFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic l in
+    let () = ComFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic ?using:atts.using l in
     pm
 
 let vernac_scheme l =
@@ -1223,21 +1251,6 @@ let vernac_set_end_tac ~pstate tac =
   (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
   Declare.Proof.set_endline_tactic tac pstate
 
-let vernac_set_used_variables ~pstate e : Declare.Proof.t =
-  let env = Global.env () in
-  let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in
-  let tys = List.map snd (initial_goals (Declare.Proof.get pstate)) in
-  let tys = List.map EConstr.Unsafe.to_constr tys in
-  let l = Proof_using.process_expr env e tys in
-  let vars = Environ.named_context env in
-  List.iter (fun id ->
-    if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then
-      user_err ~hdr:"vernac_set_used_variables"
-        (str "Unknown variable: " ++ Id.print id))
-    l;
-  let _, pstate = Declare.Proof.set_used_variables pstate l in
-  pstate
-
 (*****************************)
 (* Auxiliary file management *)