From 296faec482d17f9bfdc419f79ed565ecd8035e60 Mon Sep 17 00:00:00 2001
From: barras
Date: Thu, 7 Feb 2002 16:07:34 +0000
Subject: petit nettoyage de kernel/inductive

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2460 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/proof_trees.mli | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'proofs/proof_trees.mli')

diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index 200adac0ac..d6a1a51d5f 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -42,9 +42,8 @@ val get_hyps  : named_context sigma -> named_context
 val get_env   : named_context sigma -> env
 val get_gc    : named_context sigma -> evar_map
 
-val pf_lookup_name_as_renamed : 
-  named_context -> constr -> identifier -> int option
-val pf_lookup_index_as_renamed : constr -> int -> int option
+val pf_lookup_name_as_renamed  : env -> constr -> identifier -> int option
+val pf_lookup_index_as_renamed : env -> constr -> int -> int option
 
 
 (*s Pretty printing functions. *)
-- 
cgit v1.2.3