diff options
| author |  Jason Gross <jasongross9@gmail.com> | 2016-11-21 15:05:26 -0500 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2016-11-21 15:05:26 -0500 |
| commit | 27190db7f119bc9b50150be6dff889986c747e38 (patch) | |
| tree | 959f62953bf9d2928489aa53bf67e6288621a172 | |
| parent | aa86963464045d61fa0eaf3a7fe67ced7a6a73f4 (diff) | |
(v8.6) Add example in dev/doc/changes involving Tacmach.project
| -rw-r--r-- | dev/doc/changes.txt | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index d052468f9..e92667469 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -244,6 +244,10 @@ define_evar_* mostly used internally in the unification engine. ... let Sigma (xn, sigma, pn) = ... in Sigma (ans, sigma, p1 +> ... +> pn) + + Examples of `Sigma.Unsafe.of_evar_map` include: + + Evarutil.new_evar env (Tacmach.project goal) ty ----> Evarutil.new_evar env (Sigma.Unsafe.of_evar_map (Tacmach.project goal)) ty - The Proofview.Goal.*enter family of functions now takes a polymorphic continuation given as a record as an argument. |