From 3fe7c7879fb36cdcad5632fb20f893670db7c88c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 26 Dec 2000 11:06:40 +0000
Subject: Elimination des coupures

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1222 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tacmach.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 4df69a0cdd..ae0469a504 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -58,7 +58,7 @@ let pf_get_hyp_typ gls id =
   with Not_found -> 
     error ("No such hypothesis : " ^ (string_of_id id))
 
-let pf_ids_of_hyps gls = ids_of_named_context (named_context (pf_env gls))
+let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls)
 
 let pf_ctxt gls      = get_ctxt (sig_it gls)
 
-- 
cgit v1.2.3