aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-04-13 13:19:43 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-04-15 04:16:43 +0200
commitfc13ad4128b2d75a459829556669a59c10e8e1fe (patch)
tree98b5d48be320e7a63a3ce1a517eb03898275a9e2
parentc291a8829556dc2a61fcacc08b34e1d68d66b89e (diff)
[doc] [engine] Document `abort_on_undefined_evars`.
-rw-r--r--dev/doc/changes.md13
1 files changed, 12 insertions, 1 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 1a24f23e5..2bad21bb2 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -5,7 +5,18 @@
Proof engine
More functions have been changed to use `EConstr`, notably the
- functions in `Evd`.
+ functions in `Evd`, and in particular `Evd.define`.
+
+ Note that the core function `EConstr.to_constr` now _enforces_ by
+ default that the resulting term is ground, that is to say, free of
+ Evars. This is usually what you want, as open terms should be of
+ type `EConstr.t` to benefit from the invariants the `EConstr` API is
+ meant to guarantee.
+
+ In case you'd like to violate this API invariant, you can use the
+ `abort_on_undefined_evars` flag to `EConstr.to_constr`, but note
+ that setting this flag to false is deprecated so it is only meant to
+ be used as to help port pre-EConstr code.
## Changes between Coq 8.7 and Coq 8.8