summaryrefslogtreecommitdiff
path: root/proofs/proof_trees.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proof_trees.mli')
-rw-r--r--proofs/proof_trees.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index f9b64f41..6d1fc143 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: proof_trees.mli 9154 2006-09-20 17:18:18Z corbinea $ i*)
+(*i $Id$ i*)
(*i*)
open Util
@@ -33,7 +33,7 @@ val is_complete_proof : proof_tree -> bool
val is_leaf_proof : proof_tree -> bool
val is_tactic_proof : proof_tree -> bool
-val pf_lookup_name_as_renamed : env -> constr -> identifier -> int option
+val pf_lookup_name_as_displayed : env -> constr -> identifier -> int option
val pf_lookup_index_as_renamed : env -> constr -> int -> int option
val is_proof_instr : rule -> bool