From 454a10da9412a5bd6f3661b1f60e17f08289d0e5 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 16 Oct 2020 17:13:14 +0200
Subject: [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.
---
 proofs/proof.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'proofs/proof.ml')

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
-- 
cgit v1.2.3


From 2ac3d11f6f1332250e918ef628eca3b788b3550a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 16 Oct 2020 20:06:26 +0200
Subject: [environ] [typing_flags] Introduce helper function to remove
 duplicate code

---
 proofs/proof.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/proof.ml')

diff --git a/proofs/proof.ml b/proofs/proof.ml
index e9c8ce6746..50a0e63700 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -563,7 +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 env = Environ.update_typing_flags ?typing_flags:pr.typing_flags env in
     let (p,(status,info),()) = run_tactic env tac pr in
     let env = Global.env () in
     let sigma = Evd.from_env env in
-- 
cgit v1.2.3