From 4929fa8a5b65bd90207f3a943227ed09a7ed0b6c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 29 Jan 2013 18:15:05 +0000
Subject: Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env
 for better uniformity of naming policy.

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

(limited to 'proofs')

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 8f75133713..71a07326f9 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -36,7 +36,7 @@ let define_and_solve_constraints evk c evd =
 let w_refine (evk,evi) (ltac_var,rawc) sigma =
   if Evd.is_defined sigma evk then
     error "Instantiate called on already-defined evar";
-  let env = Evd.evar_env evi in
+  let env = Evd.evar_filtered_env evi in
   let sigma',typed_c =
     try Pretyping.understand_ltac ~resolve_classes:true true 
       sigma env ltac_var (Pretyping.OfType (Some evi.evar_concl)) rawc
@@ -53,7 +53,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
 (* Main component of vernac command Existential *)
 let instantiate_pf_com evk com sigma =
   let evi = Evd.find sigma evk in
-  let env = Evd.evar_env evi in
+  let env = Evd.evar_filtered_env evi in
   let rawc = Constrintern.intern_constr sigma env com in
   let sigma' = w_refine (evk,evi) (([],[]),rawc) sigma in
   sigma'
diff --git a/proofs/goal.ml b/proofs/goal.ml
index a9aa4fa598..df3f6e0dbd 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -464,17 +464,17 @@ module V82 = struct
   (* Old style env primitive *)
   let env evars gl =
     let evi = content evars gl in
-    Evd.evar_env evi
+    Evd.evar_filtered_env evi
 
   (* For printing *)
   let unfiltered_env evars gl =
     let evi = content evars gl in
-    Evd.evar_unfiltered_env evi
+    Evd.evar_env evi
 
   (* Old style hyps primitive *)
   let hyps evars gl =
     let evi = content evars gl in
-    evi.Evd.evar_hyps
+    Evd.evar_hyps evi
 
   (* Access to ".evar_concl" *)
   let concl evars gl =
-- 
cgit v1.2.3