Commit 04acb47f authored by MARCHE Claude's avatar MARCHE Claude

document new exported function

parent 4ae4d639
......@@ -546,7 +546,7 @@ let graft_proof_attempt ?file (s : session) (id : proofNodeID) (pr : Whyconf.pro
let pa = { pa with limit = limit;
proof_state = None;
proof_obsolete = false} in
Hprover.replace pn.proofn_attempts pr id;
(* Hprover.replace pn.proofn_attempts pr id; useless *)
Hint.replace s.proofAttempt_table id pa;
id
with Not_found ->
......
......@@ -207,6 +207,10 @@ val update_proof_attempt : ?obsolete:bool -> session -> proofNodeID ->
val apply_trans_to_goal :
allow_no_effect:bool -> session -> Env.env -> string -> string list ->
proofNodeID -> Task.task list
(** [apply_trans_to_goal s env tr args id] applies the transformation
[tr] with arguments [args] to the goal [id], and returns the
subtasks. raises [Exit] if [allow_no_effect] is false and [tr]
returns the task unchanged *)
val graft_transf : session -> proofNodeID -> string -> string list ->
Task.task list -> transID
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment