diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-23 14:58:46 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-23 14:58:46 +0200 |
| commit | 8e9d08f99c2058ed03df6b0135ec1661130e85e5 (patch) | |
| tree | cff735811cf0c4faf9462b4464a1f42e57062f14 /dev/doc | |
| parent | dfbf22a098e8e2890d2e10da5d669d9960ef6771 (diff) | |
| parent | fc13ad4128b2d75a459829556669a59c10e8e1fe (diff) | |
Merge PR #7240: [doc] [engine] Document `abort_on_undefined_evars`.
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/changes.md | 13 |
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 |