diff options
| -rw-r--r-- | dev/doc/changes.txt | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 94bde59f7..4135ddd2d 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -150,6 +150,36 @@ define_evar_* mostly used internally in the unification engine. Proofview.Refine.* ---> Refine.* +- A statically monotonous evarmap type was introduced in Sigma. Not all the API + has been converted, so that the user may want to use compatibility functions + Sigma.to_evar_map and Sigma.Unsafe.of_evar_map or Sigma.Unsafe.of_pair when + needed. Code can be straightforwardly adapted in the following way: + + let (sigma, x1) = ... in + ... + let (sigma, xn) = ... in + (sigma, ans) + + should be turned into: + + open Sigma.Notations + + let Sigma (x1, sigma, p1) = ... in + ... + let Sigma (xn, sigma, pn) = ... in + Sigma (ans, sigma, p1 +> ... +> pn) + +- The Proofview.Goal.*enter family of functions now takes a polymorphic + continuation given as a record as an argument. + + Proofview.Goal.enter begin fun gl -> ... end + + should be turned into + + open Proofview.Notations + + Proofview.Goal.enter { enter = begin fun gl -> ... end } + ========================================= = CHANGES BETWEEN COQ V8.4 AND COQ V8.5 = ========================================= |