← Back to branch summary

~naesten/coq/trunk

« back to all changes in this revision

Viewing changes to proofs/proof_trees.mli

  • Committer: herbelin
  • Date: 2009-11-09 18:05:13 UTC
  • Revision ID: svn-v4:85f007b7-540e-0410-9357-904b9bb8a0f7:trunk:12485
A bit of cleaning around name generation + creation of dedicated file namegen.ml

Show diffs side-by-side

added added

removed removed

Lines of Context:
proofs/proof_trees.mli
33
33
val is_leaf_proof     : proof_tree -> bool
34
34
val is_tactic_proof   : proof_tree -> bool
35
35
 
36
 
val pf_lookup_name_as_renamed  : env -> constr -> identifier -> int option
 
36
val pf_lookup_name_as_displayed  : env -> constr -> identifier -> int option
37
37
val pf_lookup_index_as_renamed : env -> constr -> int -> int option
38
38
 
39
39
val is_proof_instr : rule -> bool