backport changelog

Changelog.md

@@ -1,4 +1,36 @@
 # Changelog
+## [1.6.0~v8.11] - 25-08-2020
+
+Requires Elpi 1.11 and Coq 8.11.
+
+### UIs
+- Display failures generated by `std.assert!` as errors
+
+### Derive
+- Use the new `coq.elaborate-skeleton` API to insert coercions
+
+### Fix
+- Embedding for sorts was incorrectly mapping `Prop` to `sprop`
+- `coq.env.add-const` made 8.12 friendly with a workaround for coq/coq#12759
+
+### API
+- New `coq.elaborate-skeleton` and `coq.elaborate-ty-skeleton` that run
+  Coq's elaborator on a term obtained by disregarding evars and universes
+  in the given input. Unfortunately Coq's elaborator does not take terms
+  as input, but glob terms, and the conversion function is not lossless.
+  See also `lib:elpi.hole`.
+- New `coq.elaborate-indt-decl-skeleton` to elaborate an inductive type
+  declaration.
+- New `coq.elaborate-arity-skeleton` to elaborate an arity.
+- New `coq.env.current-path` to get the current module path.
+- New `coq.modpath->path` and `coq.modpath->path` to get access to the
+  components of a module path.
+- Change `coq.elpi.accumulate` understands the `@local!` attribute, which makes
+  the clauses `Local` to the module into which they live.
+
+### HOAS
+- New `lib:elpi.hole` constant that can be used in place of a unification
+  variable to denote an implicit argument when calling `coq.*-skeleton` APIs
 
 ## [1.5.0] - 29-07-2020