diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-12-07 12:28:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-12-07 12:28:14 +0100 |
| commit | ad768e435a736ca51ac79a575967b388b34918c7 (patch) | |
| tree | 6f87c9bc585d15862b66c39feb3a5172e468f67f /dev | |
| parent | cf8ecf83b5cc52f7ea73dc1d3af59bf03deff688 (diff) | |
| parent | 40cffd816b7adbf8f136f62f6f891fb5be9b96a6 (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/changes.txt | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 5fe88bf33..f54f3fcc8 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -270,6 +270,8 @@ val get_id_for_feedback : unit -> edit_or_state_id * route_id for constructing compound entries still works over this scheme. Note that in the case of (VERNAC) ARGUMENT EXTEND, the name of the argument entry is bound in the parsing rules, so beware of recursive calls. + + For example, to get "wit_constr" you must "open Constrarg" at the top of the file. - Evarutil was split in two parts. The new Evardefine file exposes functions define_evar_* mostly used internally in the unification engine. @@ -296,6 +298,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. @@ -308,7 +314,11 @@ define_evar_* mostly used internally in the unification engine. Proofview.Goal.enter { enter = begin fun gl -> ... end } -- `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)` --> `Tacinterp.Value.of_constr c` +- `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)` ---> `Tacinterp.Value.of_constr c` +- `Vernacexpr.HintsResolveEntry(priority, poly, hnf, path, atom)` ---> `Vernacexpr.HintsResolveEntry(Vernacexpr.({hint_priority = priority; hint_pattern = None}), poly, hnf, path, atom)` +- `Pretyping.Termops.mem_named_context` ---> `Engine.Termops.mem_named_context_val` + (`Global.named_context` ---> `Global.named_context_val`) + (`Context.Named.lookup` ---> `Environ.lookup_named_val`) ** Search API ** |