diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-12-02 17:46:03 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-12-02 17:46:03 +0100 |
| commit | 9dfbf93bf1d587d330b62b4f551c499f18a470e9 (patch) | |
| tree | cc9d38ad3ef1c153be0dfb800f47320a7e586bef /dev/doc | |
| parent | e83ffcd53acdebfbbd927b3c9b48a0d1ad6ca9e5 (diff) | |
| parent | 27190db7f119bc9b50150be6dff889986c747e38 (diff) | |
Merge remote-tracking branch 'github/pr/368' into v8.6
Was PR#368: Add example in dev/doc/changes involving Tacmach.project
Diffstat (limited to 'dev/doc')
| -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 83bbba96b..038aea716 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -246,6 +246,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. |