From ae6c56036f05b10b8ec728f474f4fe04ba90c752 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 8 Apr 2011 14:23:53 +0000
Subject: Applying Tom Prince's patch for build_constant_by_tactic not able to
 use a lemma name chosen by the caller (here tclABSTRACT)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13972 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/pfedit.ml  | 6 +++---
 proofs/pfedit.mli | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 6466bb8661..fff1a121d6 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -150,8 +150,7 @@ open Decl_kinds
 
 let next = let n = ref 0 in fun () -> incr n; !n
 
-let build_constant_by_tactic sign typ tac =
-  let id = id_of_string ("temporary_proof"^string_of_int (next())) in
+let build_constant_by_tactic id sign typ tac =
   start_proof id (Global,Proof Theorem) sign typ (fun _ _ -> ());
   try
     by tac;
@@ -163,5 +162,6 @@ let build_constant_by_tactic sign typ tac =
     raise e
 
 let build_by_tactic typ tac =
+  let id = id_of_string ("temporary_proof"^string_of_int (next())) in
   let sign = Decls.clear_proofs (Global.named_context ()) in
-  (build_constant_by_tactic sign typ tac).const_entry_body
+  (build_constant_by_tactic id sign typ tac).const_entry_body
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index dde52d0ccb..c16445ba3c 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -180,6 +180,6 @@ val instantiate_nth_evar_com : int -> Topconstr.constr_expr -> 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 ->
+val build_constant_by_tactic : identifier -> named_context_val -> types -> tactic ->
   Entries.definition_entry
 val build_by_tactic : types -> tactic -> constr
-- 
cgit v1.2.3