summaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2011-04-19 16:47:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2011-04-19 16:47:51 +0200
commitaa33547c764a229e22d323ca213d46ea221b903e (patch)
tree3894cb190f34bc1d2deee4322a674db641562ee0 /proofs
parent50dc9067e98ca001ad2e875011abab5da6fdb621 (diff)
parent9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 (diff)
Remove non-DFSG contentsupstream/8.3.pl2+dfsg
Diffstat (limited to 'proofs')
-rw-r--r--proofs/pfedit.ml8
-rw-r--r--proofs/pfedit.mli4
2 files changed, 6 insertions, 6 deletions
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