Merge PR #10446: [proof] Remove sign parameter to open_lemma.

Reviewed-by: SkySkimmer

6 files changed, 13 insertions, 21 deletions

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index f4edbda04a..cab82f7067 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1413,7 +1413,6 @@ let com_terminate
     let info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:Decls.(IsProof Lemma) () in
     let lemma = Lemmas.start_lemma ~name:thm_name
         ~poly:false (*FIXME*)
-        ~sign:(Environ.named_context_val env)
         ~info
         ctx
         (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) in
@@ -1451,7 +1450,7 @@ let start_equation (f:GlobRef.t) (term_f:GlobRef.t)
                              Array.of_list (List.map mkVar x)))));
     observe_tac (fun _ _ -> str "prove_eq") (cont_tactic x)]) g;;
 
-let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type =
+let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type =
     let open CVars in
     let opacity =
       match terminate_ref with
@@ -1461,7 +1460,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
     let evd = Evd.from_ctx uctx in
     let f_constr = constr_of_monomorphic_global f_ref in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
-    let lemma = Lemmas.start_lemma ~name:eq_name ~poly:false ~sign evd
+    let lemma = Lemmas.start_lemma ~name:eq_name ~poly:false evd
        (EConstr.of_constr equation_lemma_type) in
     let lemma = fst @@ Lemmas.by
        (Proofview.V82.tactic (start_equation f_ref terminate_ref
@@ -1553,9 +1552,8 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type
     (*     message "start second proof"; *)
     let stop =
       (* XXX: What is the correct way to get sign at hook time *)
-      let sign = Environ.named_context_val Global.(env ()) in
       try
-        com_eqn sign uctx (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type);
+        com_eqn uctx (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type);
         false
       with e when CErrors.noncritical e ->
         begin
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index c7b8b13282..0c45ff11d7 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -53,7 +53,7 @@ type program_info =
   ; prg_reduce : constr -> constr
   ; prg_hook : DeclareDef.Hook.t option
   ; prg_opaque : bool
-  ; prg_sign : named_context_val }
+  }
 
 (* Saving an obligation *)
 
diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli
index 7433888cec..a8dd5040cb 100644
--- a/vernac/declareObl.mli
+++ b/vernac/declareObl.mli
@@ -48,7 +48,7 @@ type program_info =
   ; prg_reduce : constr -> constr
   ; prg_hook : DeclareDef.Hook.t option
   ; prg_opaque : bool
-  ; prg_sign : Environ.named_context_val }
+  }
 
 val declare_obligation :
      program_info
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 3402e05af8..00316bfadf 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -218,9 +218,11 @@ let initialize_named_context_for_proof () =
 (* Starting a goal *)
 let start_lemma ~name ~poly
     ?(udecl=UState.default_univ_decl)
-    ?(sign=initialize_named_context_for_proof())
     ?(info=Info.make ())
     sigma c =
+  (* We remove the bodies of variables in the named context marked
+     "opaque", this is a hack tho, see #10446 *)
+  let sign = initialize_named_context_for_proof () in
   let goals = [ Global.env_of_context sign , c ] in
   let proof = Proof_global.start_proof sigma ~name ~udecl ~poly goals in
   { proof ; info }
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 17003bed7b..fbf91b3ad4 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -80,7 +80,6 @@ val start_lemma
   :  name:Id.t
   -> poly:bool
   -> ?udecl:UState.universe_decl
-  -> ?sign:Environ.named_context_val
   -> ?info:Info.t
   -> Evd.evar_map
   -> EConstr.types
@@ -122,11 +121,6 @@ val start_lemma_com
   -> Vernacexpr.proof_expr list
   -> t
 
-(* Prepare global named context for proof session: remove proofs of
-   opaque section definitions and remove vm-compiled code *)
-
-val initialize_named_context_for_proof : unit -> Environ.named_context_val
-
 (** {4 Saving proofs} *)
 
 val save_lemma_admitted : lemma:t -> unit
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index eb1e3b74b4..37fe0df0ee 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -298,7 +298,7 @@ let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
 let add_hint local prg cst =
   Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst)
 
-let init_prog_info ?(opaque = false) ?hook sign n udecl b t ctx deps fixkind
+let init_prog_info ?(opaque = false) ?hook n udecl b t ctx deps fixkind
                    notations obls impls ~scope ~poly ~kind reduce =
   let obls', b =
     match b with
@@ -335,7 +335,7 @@ let init_prog_info ?(opaque = false) ?hook sign n udecl b t ctx deps fixkind
     ; prg_reduce = reduce
     ; prg_hook = hook
     ; prg_opaque = opaque
-    ; prg_sign = sign }
+    }
 
 let map_cardinal m =
   let i = ref 0 in
@@ -495,7 +495,7 @@ let rec solve_obligation prg num tac =
   let hook = DeclareDef.Hook.make (obligation_hook prg obl num auto) in
   let info = Lemmas.Info.make ~hook ~proof_ending ~scope ~kind () in
   let poly = prg.prg_poly in
-  let lemma = Lemmas.start_lemma ~sign:prg.prg_sign ~name:obl.obl_name ~poly ~info evd (EConstr.of_constr obl.obl_type) in
+  let lemma = Lemmas.start_lemma ~name:obl.obl_name ~poly ~info evd (EConstr.of_constr obl.obl_type) in
   let lemma = fst @@ Lemmas.by !default_tactic lemma in
   let lemma = Option.cata (fun tac -> Lemmas.set_endline_tactic tac lemma) lemma tac in
   lemma
@@ -634,9 +634,8 @@ let show_term n =
 let add_definition ~name ?term t ctx ?(univdecl=UState.default_univ_decl)
                    ?(implicits=[]) ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?tactic
     ?(reduce=reduce) ?hook ?(opaque = false) obls =
-  let sign = Lemmas.initialize_named_context_for_proof () in
   let info = Id.print name ++ str " has type-checked" in
-  let prg = init_prog_info sign ~opaque name univdecl term t ctx [] None [] obls implicits ~poly ~scope ~kind reduce ?hook in
+  let prg = init_prog_info ~opaque name univdecl term t ctx [] None [] obls implicits ~poly ~scope ~kind reduce ?hook in
   let obls,_ = prg.prg_obligations in
   if Int.equal (Array.length obls) 0 then (
     Flags.if_verbose Feedback.msg_info (info ++ str ".");
@@ -654,11 +653,10 @@ let add_definition ~name ?term t ctx ?(univdecl=UState.default_univ_decl)
 let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
                            ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?(reduce=reduce)
     ?hook ?(opaque = false) notations fixkind =
-  let sign = Lemmas.initialize_named_context_for_proof () in
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
     List.iter
     (fun  (n, b, t, imps, obls) ->
-     let prg = init_prog_info sign ~opaque n univdecl (Some b) t ctx deps (Some fixkind)
+     let prg = init_prog_info ~opaque n univdecl (Some b) t ctx deps (Some fixkind)
        notations obls imps ~poly ~scope ~kind reduce ?hook
      in progmap_add n (CEphemeron.create prg)) l;
     let _defined =