From fc13ad4128b2d75a459829556669a59c10e8e1fe Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 13 Apr 2018 13:19:43 +0200 Subject: [doc] [engine] Document `abort_on_undefined_evars`. --- dev/doc/changes.md | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) (limited to 'dev/doc') 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 -- cgit v1.2.3