From e0fd7c668bc284924c63a1f0a0e36fb4856c49e1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 27 Oct 2017 16:04:00 +0200
Subject: Adding a command to evaluate Ltac2 expressions.

---
 doc/ltac2.md | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'doc')

diff --git a/doc/ltac2.md b/doc/ltac2.md
index d7c8719a14..6cbe0988d0 100644
--- a/doc/ltac2.md
+++ b/doc/ltac2.md
@@ -727,6 +727,20 @@ foo 0 ↦ (fun x => x ()) (fun _ => 0)
 Note that abbreviations are not typechecked at all, and may result in typing
 errors after expansion.
 
+# Evaluation
+
+Ltac2 features a toplevel loop that can be used to evaluate expressions.
+
+```
+VERNAC ::=
+| "Ltac2" "Eval" TERM
+```
+
+This command evaluates the term in the current proof if there is one, or in the
+global environment otherwise, and displays the resulting value to the user
+together with its type. This function is pure in the sense that it does not
+modify the state of the proof, and in particular all side-effects are discarded.
+
 # Debug
 
 When the option `Ltac2 Backtrace` is set, toplevel failures will be printed with
-- 
cgit v1.2.3