aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqloop.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-10-11 20:49:57 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-10-17 20:14:13 +0200
commitf4045c5bfc2318792af87971ddfa08df16df8961 (patch)
tree95905c242c962b73f6cde5f5feec4f65fc9f2272 /toplevel/coqloop.ml
parentf3d1eff69850d379bad5ab8f1cdadb7f5d5c7eca (diff)
Applying Emilio's suggestion to simplify type of eval_expr.
This is not fully satisfactory though since we would not like to have "eval_expr" depending on a parsing/lexing/comments state... but it does because of eval_expr possibly printing the vernac expression given to it.
Diffstat (limited to 'toplevel/coqloop.ml')
-rw-r--r--toplevel/coqloop.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 71e1f9593..08c3fe205 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -299,7 +299,7 @@ let do_vernac () =
resynch_buffer top_buffer;
try
let input = (top_buffer.tokens, None) in
- Vernac.eval_expr input (read_sentence input)
+ Vernac.eval_expr top_buffer.tokens (read_sentence input)
with
| End_of_input | CErrors.Quit ->
top_stderr (fnl ()); raise CErrors.Quit