aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq_commands.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coq_commands.ml')
-rw-r--r--ide/coq_commands.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index a8edc4061..fdaee4508 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -156,6 +156,8 @@ let commands = [
let state_preserving = [
"Check";
"Eval";
+ "Eval lazy in";
+ "Eval vm_compute in";
"Eval compute in";
"Extraction";
"Extraction Library";