From 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Tue, 19 Apr 2011 16:44:20 +0200
Subject: Imported Upstream version 8.3.pl2

---
 proofs/pfedit.ml  | 8 ++++----
 proofs/pfedit.mli | 4 ++--
 2 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 171db848..42111213 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pfedit.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: pfedit.ml 13981 2011-04-08 16:59:26Z herbelin $ *)
 
 open Pp
 open Util
@@ -344,8 +344,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;
@@ -357,5 +356,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 1b284f8d..8df26706 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pfedit.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: pfedit.mli 13981 2011-04-08 16:59:26Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -202,6 +202,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 ->
+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