aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/goal.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/goal.mli')
-rw-r--r--proofs/goal.mli3
1 files changed, 0 insertions, 3 deletions
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 6d3ec8bd4..ad968cdfb 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -15,9 +15,6 @@ type goal = Evar.t
(* Gives a unique identifier to each goal. The identifier is
guaranteed to contain no space. *)
val uid : goal -> string
-(* Returns the goal (even if it has been partially solved)
- corresponding to a unique identifier obtained by {!uid}. *)
-val get_by_uid : string -> goal
(* Debugging help *)
val pr_goal : goal -> Pp.t