From 8e150e9ccf3ecc81fa3b782297cccea3f9d1854b Mon Sep 17 00:00:00 2001
From: corbinea
Date: Wed, 30 Jun 2004 11:32:28 +0000
Subject: updated printing of evar context (may loop ?)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5857 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/evar_refiner.ml | 2 +-
 proofs/proof_trees.ml  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index b04691d87b..719d95aedc 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -153,7 +153,7 @@ let instantiate_pf_com n com pfts =
   let sigma = (w_Underlying wc) in 
   let (sp,evd) (* as evc *) = 
     try
-      List.nth (Evd.non_instantiated sigma) (n-1) 
+      List.nth (Evarutil.non_instantiated sigma) (n-1) 
     with Failure _ -> 
       error "not so many uninstantiated existential variables"
   in 
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 6358b71892..271592b73a 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -229,7 +229,7 @@ let rec pr_evars_int i = function
 
 let pr_subgoals_existential sigma = function 
   | [] -> 
-      let exl = Evd.non_instantiated sigma in 
+      let exl = non_instantiated sigma in 
       if exl = [] then 
 	(str"Proof completed."  ++ fnl ())
       else
-- 
cgit v1.2.3