From 96e78e0d4ab9e2c2ccf1bb0565384e4e0d322904 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 22 Jun 2018 00:43:01 +0200 Subject: Move transparent_state to its own module. --- dev/top_printers.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dev') diff --git a/dev/top_printers.mli b/dev/top_printers.mli index 63d7d58053..5876b7c5c6 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -101,7 +101,7 @@ val ppdelta : Mod_subst.delta_resolver -> unit val pp_idpred : Names.Id.Pred.t -> unit val pp_cpred : Names.Cpred.t -> unit -val pp_transparent_state : Names.transparent_state -> unit +val pp_transparent_state : TranspState.t -> unit val pp_stack_t : Constr.t Reductionops.Stack.t -> unit val pp_cst_stack_t : Reductionops.Cst_stack.t -> unit -- cgit v1.2.3 From ad5aea737ecc639c31dda84322b3550a4d380b47 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 22 Jun 2018 21:06:01 +0200 Subject: Proper record type and accessors for transparent states. This is documented in dev/doc/changes.md. --- dev/doc/changes.md | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'dev') diff --git a/dev/doc/changes.md b/dev/doc/changes.md index b1fdfafd3a..9c5785758d 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -19,6 +19,10 @@ Names Constant.make3 has been removed, use Constant.make2 Constant.repr3 has been removed, use Constant.repr2 +- `Names.transparent_state` has been moved to its own module `TranspState`. + This module gathers utility functions that used to be defined in several + places. + Coqlib: - Most functions from the `Coqlib` module have been deprecated in favor of -- cgit v1.2.3 From 733cb74a2038ff92156b7209713fc2ea741ccca6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 19 Nov 2018 08:12:28 +0100 Subject: Rename TranspState into TransparentState. --- dev/doc/changes.md | 2 +- dev/top_printers.mli | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'dev') diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 9c5785758d..30a2967259 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -19,7 +19,7 @@ Names Constant.make3 has been removed, use Constant.make2 Constant.repr3 has been removed, use Constant.repr2 -- `Names.transparent_state` has been moved to its own module `TranspState`. +- `Names.transparent_state` has been moved to its own module `TransparentState`. This module gathers utility functions that used to be defined in several places. diff --git a/dev/top_printers.mli b/dev/top_printers.mli index 5876b7c5c6..eaa12ff702 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -101,7 +101,7 @@ val ppdelta : Mod_subst.delta_resolver -> unit val pp_idpred : Names.Id.Pred.t -> unit val pp_cpred : Names.Cpred.t -> unit -val pp_transparent_state : TranspState.t -> unit +val pp_transparent_state : TransparentState.t -> unit val pp_stack_t : Constr.t Reductionops.Stack.t -> unit val pp_cst_stack_t : Reductionops.Cst_stack.t -> unit -- cgit v1.2.3 From 58926ede84b84b2fb51e3d159872e1aaad339bf7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 19 Oct 2018 15:58:35 +0200 Subject: Adding overlays. --- dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh (limited to 'dev') diff --git a/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh b/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh new file mode 100644 index 0000000000..b05d02c5be --- /dev/null +++ b/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh @@ -0,0 +1,14 @@ +_OVERLAY_BRANCH=clean-transp-state + +if [ "$CI_PULL_REQUEST" = "7925" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then + + unicoq_CI_REF="$_OVERLAY_BRANCH" + unicoq_CI_GITURL=https://github.com/ppedrot/unicoq + + equations_CI_REF="$_OVERLAY_BRANCH" + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + + mtac2_CI_REF="$_OVERLAY_BRANCH" + mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 + +fi -- cgit v1.2.3