Stop accessing proof env via Pfedit in printers

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

1 files changed, 27 insertions, 27 deletions

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