aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/coq.ml2
-rw-r--r--ide/coqide.ml2
2 files changed, 2 insertions, 2 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index cccd911144..6e447df1de 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -244,7 +244,7 @@ let reset_to id =
Vernacentries.abort_refine Lib.reset_name (Util.dummy_loc,id)
let reset_to_mod id =
prerr_endline ("Reset called to Mod/Sect with "^(string_of_id id));
- Lib.reset_mod (Util.dummy_loc,id)
+ Vernacentries.abort_refine Lib.reset_mod (Util.dummy_loc,id)
let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) =
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 5abc2c6e14..0b87f41cb1 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -457,7 +457,7 @@ let update_on_end_of_proof id =
r := true; raise Exit end
else begin
prerr_endline "Toggling Changing Reset id";
- r:=false
+ r := false
end
| { ast = _, (VernacAbort _ | VernacAbortAll) } -> raise Exit
| _ -> ()