[printing] Deprecate all printing functions accessing the global proof.

We'd like to handle proofs functionally we thus recommend not to use
printing functions without an explicit context.

We also adapt most of the code, making more explicit where the
printing environment is coming from.

An open task is to refactor some code so we gradually make the
`Pfedit.get_current_context ()` disappear.

1 files changed, 13 insertions, 10 deletions

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 218342efe..cb54cac3f 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -984,7 +984,9 @@ struct
 
   let parse_expr sigma parse_constant parse_exp ops_spec env term =
     if debug
-    then Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr term);
+    then (
+      let _, env = Pfedit.get_current_context () in
+      Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env env sigma term));
 
 (*
     let constant_or_variable env term =
@@ -1103,9 +1105,10 @@ struct
     |  _ -> raise ParseError
 
 
-  let rconstant sigma term = 
+  let rconstant sigma term =
+    let _, env = Pfedit.get_current_context () in
     if debug
-    then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr term ++ fnl ());
+    then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr_env env sigma term ++ fnl ());
     let res = rconstant sigma term in
       if debug then 
 	(Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ;
@@ -1145,9 +1148,9 @@ struct
 
   let  parse_arith parse_op parse_expr env cstr gl =
     let sigma = gl.sigma in
-   if debug
-   then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr cstr ++ fnl ());
-   match EConstr.kind sigma cstr with
+    if debug
+    then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr_env gl.env sigma cstr ++ fnl ());
+    match EConstr.kind sigma cstr with
     | Term.App(op,args) ->
        let (op,lhs,rhs) = parse_op gl (op,args) in
        let (e1,env) = parse_expr sigma env lhs in
@@ -1908,7 +1911,7 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
      let formula_typ = (EConstr.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in
      let ff = dump_formula formula_typ
        (dump_cstr spec.typ spec.dump_coeff) ff in
-       Feedback.msg_notice (Printer.pr_leconstr ff);
+       Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff);
        Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff
    end;
 
@@ -1932,9 +1935,9 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
       Feedback.msg_notice (Pp.str "\nAFormula\n") ;
       let formula_typ = (EConstr.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in
       let ff' = dump_formula formula_typ
-        (dump_cstr spec.typ spec.dump_coeff) ff' in
-        Feedback.msg_notice (Printer.pr_leconstr ff');
-        Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff'
+          (dump_cstr spec.typ spec.dump_coeff) ff' in
+      Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff');
+      Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff'
     end;
 
   (* Even if it does not work, this does not mean it is not provable