Stop accessing proof env via Pfedit in printers

This should make https://github.com/coq/coq/pull/9129 easier.

5 files changed, 53 insertions, 56 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 23cdae7883..048ec56dee 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -27,10 +27,6 @@ let init_size=5
 
 let cc_verbose=ref false
 
-let print_constr t =
-  let sigma, env = Pfedit.get_current_context () in
-  Printer.pr_econstr_env env sigma t
-
 let debug x =
   if !cc_verbose then Feedback.msg_debug (x ())
 
@@ -484,11 +480,11 @@ let rec inst_pattern subst = function
 	(fun spat f -> Appli (f,inst_pattern subst spat))
 	   args t
 
-let pr_idx_term uf i = str "[" ++ int i ++ str ":=" ++
-  print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]"
+let pr_idx_term env sigma uf i = str "[" ++ int i ++ str ":=" ++
+  Printer.pr_econstr_env env sigma (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]"
 
-let pr_term t = str "[" ++
-  print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]"
+let pr_term env sigma t = str "[" ++
+  Printer.pr_econstr_env env sigma (EConstr.of_constr (constr_of_term t)) ++ str "]"
 
 let rec add_term state t=
   let uf=state.uf in
@@ -603,16 +599,16 @@ let add_inst state (inst,int_subst) =
 	      begin
 		debug (fun () ->
 		   (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
-                  (str "  [" ++ print_constr (EConstr.of_constr prf) ++ str " : " ++
-			   pr_term s ++ str " == " ++ pr_term t ++ str "]"));
+                  (str "  [" ++ Printer.pr_econstr_env state.env state.sigma (EConstr.of_constr prf) ++ str " : " ++
+                           pr_term state.env state.sigma s ++ str " == " ++ pr_term state.env state.sigma t ++ str "]"));
 		add_equality state prf s t
 	      end
 	    else
 	      begin
 		debug (fun () ->
 		   (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
-                  (str "  [" ++ print_constr (EConstr.of_constr prf) ++ str " : " ++
-			   pr_term s ++ str " <> " ++ pr_term t ++ str "]"));
+                  (str "  [" ++ Printer.pr_econstr_env state.env state.sigma (EConstr.of_constr prf) ++ str " : " ++
+                           pr_term state.env state.sigma s ++ str " <> " ++ pr_term state.env state.sigma t ++ str "]"));
 		add_disequality state (Hyp prf) s t
 	      end
   end
@@ -640,8 +636,8 @@ let join_path uf i j=
   min_path (down_path uf i [],down_path uf j [])
 
 let union state i1 i2 eq=
-  debug (fun () -> str "Linking " ++ pr_idx_term state.uf i1 ++
-		 str " and " ++ pr_idx_term state.uf i2 ++ str ".");
+  debug (fun () -> str "Linking " ++ pr_idx_term state.env state.sigma state.uf i1 ++
+                 str " and " ++ pr_idx_term state.env state.sigma state.uf i2 ++ str ".");
   let r1= get_representative state.uf i1
   and r2= get_representative state.uf i2 in
     link state.uf i1 i2 eq;
@@ -681,8 +677,8 @@ let union state i1 i2 eq=
 
 let merge eq state = (* merge and no-merge *)
   debug
-    (fun () -> str "Merging " ++ pr_idx_term state.uf eq.lhs ++
-       str " and " ++ pr_idx_term state.uf eq.rhs ++ str ".");
+    (fun () -> str "Merging " ++ pr_idx_term state.env state.sigma state.uf eq.lhs ++
+       str " and " ++ pr_idx_term state.env state.sigma state.uf eq.rhs ++ str ".");
   let uf=state.uf in
   let i=find uf eq.lhs
   and j=find uf eq.rhs in
@@ -694,7 +690,7 @@ let merge eq state = (* merge and no-merge *)
 
 let update t state = (* update 1 and 2 *)
   debug
-    (fun () -> str "Updating term " ++ pr_idx_term state.uf t ++ str ".");
+    (fun () -> str "Updating term " ++ pr_idx_term state.env state.sigma state.uf t ++ str ".");
   let (i,j) as sign = signature state.uf t in
   let (u,v) = subterms state.uf t in
   let rep = get_representative state.uf i in
@@ -756,7 +752,7 @@ let process_constructor_mark t i rep pac state =
 
 let process_mark t m state =
   debug
-    (fun () -> str "Processing mark for term " ++ pr_idx_term state.uf t ++ str ".");
+    (fun () -> str "Processing mark for term " ++ pr_idx_term state.env state.sigma state.uf t ++ str ".");
   let i=find state.uf t in
   let rep=get_representative state.uf i in
     match m with
@@ -777,8 +773,8 @@ let check_disequalities state =
           else (str "No", check_aux q)
         in
         let _ = debug
-        (fun () -> str "Checking if " ++ pr_idx_term state.uf dis.lhs ++ str " = " ++
-         pr_idx_term state.uf dis.rhs ++ str " ... " ++ info) in
+        (fun () -> str "Checking if " ++ pr_idx_term state.env state.sigma state.uf dis.lhs ++ str " = " ++
+         pr_idx_term state.env state.sigma state.uf dis.rhs ++ str " ... " ++ info) in
         ans
     | [] -> None
   in
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index d52e83dc31..978969bf59 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -169,7 +169,7 @@ val find_instances : state -> (quant_eq * int array) list
 
 val execute : bool -> state -> explanation option
 
-val pr_idx_term : forest -> int -> Pp.t
+val pr_idx_term : Environ.env -> Evd.evar_map -> forest -> int -> Pp.t
 
 val empty_forest: unit -> forest
 
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 1f1fa9c99a..4f46f8327a 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -94,65 +94,65 @@ let pinject p c n a =
    p_rhs=nth_arg p.p_rhs (n-a);
    p_rule=Inject(p,c,n,a)}
 
-let rec equal_proof uf i j=
-  debug (fun () -> str "equal_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+let rec equal_proof env sigma uf i j=
+  debug (fun () -> str "equal_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
   if i=j then prefl (term uf i) else
     let (li,lj)=join_path uf i j in
-    ptrans (path_proof uf i li) (psym (path_proof uf j lj))
+    ptrans (path_proof env sigma uf i li) (psym (path_proof env sigma uf j lj))
       
-and edge_proof uf ((i,j),eq)=
-  debug (fun () -> str "edge_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
-  let pi=equal_proof uf i eq.lhs in
-  let pj=psym (equal_proof uf j eq.rhs) in
+and edge_proof env sigma uf ((i,j),eq)=
+  debug (fun () -> str "edge_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
+  let pi=equal_proof env sigma uf i eq.lhs in
+  let pj=psym (equal_proof env sigma uf j eq.rhs) in
   let pij=
     match eq.rule with
       Axiom (s,reversed)->
 	if reversed then psymax (axioms uf) s
 	else pax (axioms uf) s
-    | Congruence ->congr_proof uf eq.lhs eq.rhs
+    | Congruence ->congr_proof env sigma uf eq.lhs eq.rhs
     | Injection (ti,ipac,tj,jpac,k) -> (* pi_k ipac = p_k jpac *) 
-      let p=ind_proof uf ti ipac tj jpac in
+      let p=ind_proof env sigma uf ti ipac tj jpac in
       let cinfo= get_constructor_info uf ipac.cnode in
       pinject p cinfo.ci_constr cinfo.ci_nhyps k in  
   ptrans (ptrans pi pij) pj
   
-and constr_proof uf i ipac=
-  debug (fun () -> str "constr_proof " ++ pr_idx_term uf i ++ brk (1,20));
+and constr_proof env sigma uf i ipac=
+  debug (fun () -> str "constr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20));
   let t=find_oldest_pac uf i ipac in
-  let eq_it=equal_proof uf i t in
+  let eq_it=equal_proof env sigma uf i t in
   if ipac.args=[] then
     eq_it
   else
     let fipac=tail_pac ipac in
     let (fi,arg)=subterms uf t in
     let targ=term uf arg in
-    let p=constr_proof uf fi fipac in
+    let p=constr_proof env sigma uf fi fipac in
     ptrans eq_it (pcongr p (prefl targ))
       
-and path_proof uf i l=
-  debug (fun () -> str "path_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ str "{" ++
+and path_proof env sigma uf i l=
+  debug (fun () -> str "path_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ str "{" ++
 	   (prlist_with_sep (fun () -> str ",") (fun ((_,j),_) -> int j) l) ++ str "}");
   match l with
   | [] -> prefl (term uf i)
-  | x::q->ptrans (path_proof uf (snd (fst x)) q) (edge_proof uf x)
+  | x::q->ptrans (path_proof env sigma uf (snd (fst x)) q) (edge_proof env sigma uf x)
     
-and congr_proof uf i j=
-  debug (fun () -> str "congr_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+and congr_proof env sigma uf i j=
+  debug (fun () -> str "congr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
   let (i1,i2) = subterms uf i
   and (j1,j2) = subterms uf j in
-  pcongr (equal_proof uf i1 j1) (equal_proof uf i2 j2)
+  pcongr (equal_proof env sigma uf i1 j1) (equal_proof env sigma uf i2 j2)
     
-and ind_proof uf i ipac j jpac=
-   debug (fun () -> str "ind_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
-  let p=equal_proof uf i j
-  and p1=constr_proof uf i ipac
-  and p2=constr_proof uf j jpac in
+and ind_proof env sigma uf i ipac j jpac=
+   debug (fun () -> str "ind_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
+  let p=equal_proof env sigma uf i j
+  and p1=constr_proof env sigma uf i ipac
+  and p2=constr_proof env sigma uf j jpac in
   ptrans (psym p1) (ptrans p p2)
 
-let build_proof uf=
+let build_proof env sigma uf=
   function
-  | `Prove (i,j) -> equal_proof uf i j
-  | `Discr (i,ci,j,cj)-> ind_proof uf i ci j cj
+  | `Prove (i,j) -> equal_proof env sigma uf i j
+  | `Discr (i,ci,j,cj)-> ind_proof env sigma uf i ci j cj
 
 
 
diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli
index bebef241e1..9ea31259c1 100644
--- a/plugins/cc/ccproof.mli
+++ b/plugins/cc/ccproof.mli
@@ -41,20 +41,20 @@ val pinject :  proof -> pconstructor -> int -> int -> proof
 
 (** Proof building functions *)
 
-val equal_proof : forest -> int -> int -> proof
+val equal_proof : Environ.env -> Evd.evar_map -> forest -> int -> int -> proof
 
-val edge_proof : forest -> (int*int)*equality -> proof
+val edge_proof : Environ.env -> Evd.evar_map -> forest -> (int*int)*equality -> proof
 
-val path_proof : forest -> int -> ((int*int)*equality) list -> proof
+val path_proof : Environ.env -> Evd.evar_map -> forest -> int -> ((int*int)*equality) list -> proof
 
-val congr_proof :  forest -> int -> int -> proof
+val congr_proof : Environ.env -> Evd.evar_map -> forest -> int -> int -> proof
 
-val ind_proof : forest -> int -> pa_constructor -> int -> pa_constructor -> proof
+val ind_proof : Environ.env -> Evd.evar_map -> forest -> int -> pa_constructor -> int -> pa_constructor -> proof
 
 (** Main proof building function *)
 
 val build_proof :
-  forest ->
+  Environ.env -> Evd.evar_map -> forest ->
   [ `Discr of int * pa_constructor * int * pa_constructor
   | `Prove of int * int ] -> proof
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 5778acce0a..50fc2448fc 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -433,7 +433,7 @@ let cc_tactic depth additionnal_terms =
 	debug (fun () -> Pp.str "Goal solved, generating proof ...");
 	match reason with
 	  Discrimination (i,ipac,j,jpac) ->
-	    let p=build_proof uf (`Discr (i,ipac,j,jpac)) in
+            let p=build_proof (Tacmach.New.pf_env gl) sigma uf (`Discr (i,ipac,j,jpac)) in
 	    let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
 	    discriminate_tac cstr p
 	| Incomplete ->
@@ -462,7 +462,8 @@ let cc_tactic depth additionnal_terms =
 		 Pp.str "  replacing metavariables by arbitrary terms.");
 	    Tacticals.New.tclFAIL 0 (str "Incomplete")
 	| Contradiction dis ->
-	    let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in
+      let env = Proofview.Goal.env gl in
+            let p=build_proof env sigma uf (`Prove (dis.lhs,dis.rhs)) in
 	    let ta=term uf dis.lhs and tb=term uf dis.rhs in
 	    match dis.rule with
 	      Goal -> proof_tac p