diff options
Diffstat (limited to 'CHANGES')
-rw-r--r-- | CHANGES | 12 |
1 files changed, 12 insertions, 0 deletions
@@ -94,6 +94,18 @@ Build Infrastructure access to the same .cmi files. In short, use "make -j && make -j byte" instead of "make -j world byte". +Universes + +- Cumulative inductive types. see prefixes "Cumulative", "NonCumulative" + for inductive definitions and the option "Set Inductive Cumulativity" + in the reference manual. + +XML Protocol + +- The `query` call has been modified, now it carries a mandatory + "route_id" integer parameter, that associated the result of such + query with its generated feedback. + Changes from V8.6beta1 to V8.6 ============================== |