A bit of cleaning around name generation + creation of dedicated file namegen.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12485 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 12 insertions, 7 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index e8ef6dd678..7895bfac93 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -342,15 +342,18 @@ open Decl_kinds
 
 let next = let n = ref 0 in fun () -> incr n; !n
 
-let build_by_tactic typ tac =
+let build_constant_by_tactic sign typ tac =
   let id = id_of_string ("temporary_proof"^string_of_int (next())) in
-  let sign = Decls.clear_proofs (Global.named_context ()) in
   start_proof id (Global,Proof Theorem) sign typ (fun _ _ -> ());
   try
     by tac;
     let _,(const,_,_,_) = cook_proof (fun _ -> ()) in
     delete_current_proof ();
-    const.const_entry_body
+    const
   with e ->
     delete_current_proof ();
     raise e
+
+let build_by_tactic typ tac =
+  let sign = Decls.clear_proofs (Global.named_context ()) in
+  (build_constant_by_tactic sign typ tac).const_entry_body
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index f46825b0c1..6acf1ff780 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -197,4 +197,6 @@ val mutate : (pftreestate -> pftreestate) -> unit
 
 (* [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *)
 
+val build_constant_by_tactic : named_context_val -> types -> tactic ->
+  Entries.definition_entry
 val build_by_tactic : types -> tactic -> constr
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index b5f46d7887..8c808e1c84 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -68,8 +68,8 @@ let is_tactic_proof pf = match pf.ref with
   | _ -> false
 
 
-let pf_lookup_name_as_renamed env ccl s =
-  Detyping.lookup_name_as_renamed env ccl s
+let pf_lookup_name_as_displayed env ccl s =
+  Detyping.lookup_name_as_displayed env ccl s
 
 let pf_lookup_index_as_renamed env ccl n =
   Detyping.lookup_index_as_renamed env ccl n
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index dcbddbd9e8..6d1fc143d3 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -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
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 754d98616f..acccfb812d 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -11,7 +11,7 @@
 open Pp
 open Util
 open Names
-open Nameops
+open Namegen
 open Sign
 open Term
 open Termops