aboutsummaryrefslogtreecommitdiff
path: root/ide/coq.mli
diff options
context:
space:
mode:
authorvgross2010-02-26 19:31:31 +0000
committervgross2010-02-26 19:31:31 +0000
commit7cb299f5c1b534246e92e99b39aa4e2b84fbb9e4 (patch)
treee00a6b0f216d952c32d103d116e38653f3275426 /ide/coq.mli
parentaf0f9fd3a43824d4e86b36a784619736478f4c83 (diff)
New backtracking code + fix bug #2082.
Previous code checkings were too lax, and information was lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12823 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coq.mli')
-rw-r--r--ide/coq.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coq.mli b/ide/coq.mli
index f571c176ab..ffa05b00a4 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -38,7 +38,7 @@ val interp : bool -> string -> int
val interp_and_replace : string ->
int * string
-val old_rewind : int -> unit
+val rewind : int -> int
val is_vernac_tactic_command : Vernacexpr.vernac_expr -> bool
val is_vernac_state_preserving_command : Vernacexpr.vernac_expr -> bool