[proofs] Support per-definition typing-flags in interactive proofs.

Most cases should be accounted in proof code, however be wary of paths
where `Global.env ()` is used.

4 files changed, 14 insertions, 8 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 24f3ac3f29..e9c8ce6746 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -115,6 +115,7 @@ type t =
   (** the name of the theorem whose proof is being constructed *)
   ; poly : bool
   (** polymorphism *)
+  ; typing_flags : Declarations.typing_flags option
   }
 
 (*** General proof functions ***)
@@ -278,7 +279,7 @@ let end_of_stack = CondEndStack end_of_stack_kind
 
 let unfocused = is_last_focus end_of_stack_kind
 
-let start ~name ~poly sigma goals =
+let start ~name ~poly ?typing_flags sigma goals =
   let entry, proofview = Proofview.init sigma goals in
   let pr =
     { proofview
@@ -286,10 +287,11 @@ let start ~name ~poly sigma goals =
     ; focus_stack = []
     ; name
     ; poly
+    ; typing_flags
   } in
   _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr
 
-let dependent_start ~name ~poly goals =
+let dependent_start ~name ~poly ?typing_flags goals =
   let entry, proofview = Proofview.dependent_init goals in
   let pr =
     { proofview
@@ -297,6 +299,7 @@ let dependent_start ~name ~poly goals =
     ; focus_stack = []
     ; name
     ; poly
+    ; typing_flags
   } in
   let number_of_goals = List.length (Proofview.initial_goals pr.entry) in
   _focus end_of_stack (Obj.repr ()) 1 number_of_goals pr
@@ -560,6 +563,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
       else tac
     in
     let env = Global.env () in
+    let env = Option.cata (fun f -> Environ.set_typing_flags f env) env pr.typing_flags in
     let (p,(status,info),()) = run_tactic env tac pr in
     let env = Global.env () in
     let sigma = Evd.from_env env in
diff --git a/proofs/proof.mli b/proofs/proof.mli
index f487595dac..a527820c7a 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -55,11 +55,13 @@ val data : t -> data
 val start
   :  name:Names.Id.t
   -> poly:bool
+  -> ?typing_flags:Declarations.typing_flags
   -> Evd.evar_map -> (Environ.env * EConstr.types) list -> t
 
 val dependent_start
   :  name:Names.Id.t
   -> poly:bool
+  -> ?typing_flags:Declarations.typing_flags
   -> Proofview.telescope -> t
 
 (* Returns [true] if the considered proof is completed, that is if no goal remain
diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v
index a6640a5a03..a5fe676cc1 100644
--- a/test-suite/success/typing_flags.v
+++ b/test-suite/success/typing_flags.v
@@ -27,13 +27,12 @@ Print Assumptions att_Cor.
 
 (* Interactive + atts *)
 
-(* Coq's handling of environments in tactic mode is too broken for this to work yet *)
+(* Coq's handling of environments in tactic mode is too broken for
+   this to work yet, the pretyper doesn't get the right flags *)
 
-(*
 #[typing(universes=no)] Definition i_att_T' : Type. Proof. exact (let t := Type in (t : t)). Defined.
 #[typing(universes=no)] Definition d_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed.
 #[typing(universes=no)] Program Definition pi_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed.
-*)
 
 (* Note: this works a bit by chance, the attribute only affects the
    kernel call in Defined. Would the tactics perform a check we would
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 4921ce0f0d..74ace04a7c 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -1428,9 +1428,9 @@ let start_proof_core ~name ~typ ~pinfo ?(sign=initialize_named_context_for_proof
      marked "opaque", this is a hack tho, see #10446, and
      build_constant_by_tactic uses a different method that would break
      program_inference_hook *)
-  let { Proof_info.info = { Info.poly; _ }; _ } = pinfo in
+  let { Proof_info.info = { Info.poly; typing_flags; _ }; _ } = pinfo in
   let goals = [Global.env_of_context sign, typ] in
-  let proof = Proof.start ~name ~poly sigma goals in
+  let proof = Proof.start ~name ~poly ?typing_flags sigma goals in
   let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
   { proof
   ; endline_tactic = None
@@ -1451,7 +1451,8 @@ let start_core ~info ~cinfo ?proof_ending sigma =
 let start = start_core ?proof_ending:None
 
 let start_dependent ~info ~name ~proof_ending goals =
-  let proof = Proof.dependent_start ~name ~poly:info.Info.poly goals in
+  let { Info.poly; typing_flags; _ } = info in
+  let proof = Proof.dependent_start ~name ~poly ?typing_flags goals in
   let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
   let cinfo = [] in
   let pinfo = Proof_info.make ~info ~cinfo ~proof_ending () in