diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/7080-herbelin-master+swapping-modules-constr-context.sh | 7 | ||||
| -rw-r--r-- | dev/doc/changes.md | 10 | ||||
| -rw-r--r-- | dev/doc/versions-history.tex | 12 | ||||
| -rw-r--r-- | dev/top_printers.ml | 2 |
4 files changed, 29 insertions, 2 deletions
diff --git a/dev/ci/user-overlays/7080-herbelin-master+swapping-modules-constr-context.sh b/dev/ci/user-overlays/7080-herbelin-master+swapping-modules-constr-context.sh new file mode 100644 index 000000000..b4d3d7e67 --- /dev/null +++ b/dev/ci/user-overlays/7080-herbelin-master+swapping-modules-constr-context.sh @@ -0,0 +1,7 @@ +if [ "$CI_PULL_REQUEST" = "7080" ] || [ "$CI_BRANCH" = "master+swapping-modules-constr-context" ]; then + Equations_CI_BRANCH=master+adapting-coq-pr7080 + Equations_CI_GITURL=https://github.com/herbelin/Coq-Equations.git + + Elpi_CI_BRANCH=coq-master+adapting-coq-pr7080 + Elpi_CI_GITURL=https://github.com/herbelin/coq-elpi.git +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 3e36b657d..e6d741159 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -53,6 +53,16 @@ Printer.ml API pr_subgoal and pr_goal was removed to simplify the code. It was earlierly used by PCoq. +Kernel + + The following renamings happened: + - `Context.Rel.t` into `Constr.rel_context` + - `Context.Named.t` into `Constr.named_context` + - `Context.Compacted.t` into `Constr.compacted_context` + - `Context.Rel.Declaration.t` into `Constr.rel_declaration` + - `Context.Named.Declaration.t` into `Constr.named_declaration` + - `Context.Compacted.Declaration.t` into `Constr.compacted_declaration` + Source code organization - We have eliminated / fused some redundant modules and relocated a diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex index 3867d4af9..8f9c3171d 100644 --- a/dev/doc/versions-history.tex +++ b/dev/doc/versions-history.tex @@ -395,7 +395,17 @@ Coq V8.7 beta 1 & released 6 September 2017 & \feature{bundled with Ssreflect pl Coq V8.7 beta 2 & released 6 October 2017 & \\ -Coq V8.7 & released 18 October 2016 & \\ +Coq V8.7.0 & released 18 October 2017 & \\ + +Coq V8.7.1 & released 15 December 2017 & \\ + +Coq V8.7.2 & released 17 February 2018 & \\ + +Coq V8.8 beta1 & released 19 March 2018 & \\ + +Coq V8.8.0 & released 17 April 2018 & \feature{reference manual moved to Sphinx} \\ +&& \feature{effort towards better documented, better structured ML API}\\ +&& \feature{miscellaneous changes/improvements of existing features}\\ \end{tabular} diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 811abd67f..ab679a71c 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -232,7 +232,7 @@ let ppenv e = pp let ppenvwithcst e = pp (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++ str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++ - str "{" ++ Cmap_env.fold (fun a _ s -> Constant.print a ++ spc () ++ s) (Obj.magic e).env_globals.env_constants (mt ()) ++ str "}") + str "{" ++ Environ.fold_constants (fun a _ s -> Constant.print a ++ spc () ++ s) e (mt ()) ++ str "}") let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x)) |