From a9f0fd89cf3bb4b728eb451572a96f8599211380 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 30 Jan 2019 14:39:28 +0100
Subject: Separate variance and universe fields in inductives.

I think the usage looks cleaner this way.
---
 dev/ci/user-overlays/09439-sep-variance.sh | 14 ++++++++++++++
 dev/include                                |  2 --
 dev/top_printers.ml                        |  2 --
 dev/top_printers.mli                       |  2 --
 4 files changed, 14 insertions(+), 6 deletions(-)
 create mode 100644 dev/ci/user-overlays/09439-sep-variance.sh

(limited to 'dev')

diff --git a/dev/ci/user-overlays/09439-sep-variance.sh b/dev/ci/user-overlays/09439-sep-variance.sh
new file mode 100644
index 0000000000..cca85a2f68
--- /dev/null
+++ b/dev/ci/user-overlays/09439-sep-variance.sh
@@ -0,0 +1,14 @@
+
+if [ "$CI_PULL_REQUEST" = "9439" ] || [ "$CI_BRANCH" = "sep-variance" ]; then
+    elpi_CI_REF=sep-variance
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+    equations_CI_REF=sep-variance
+    equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+    mtac2_CI_REF=sep-variance
+    mtac2_CI_GITURL=https://github.com/SkySkimmer/mtac2
+
+    paramcoq_CI_REF=sep-variance
+    paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
+fi
diff --git a/dev/include b/dev/include
index b982f4c9fa..c5de83b900 100644
--- a/dev/include
+++ b/dev/include
@@ -41,8 +41,6 @@
 #install_printer  (* univ context *) ppuniverse_context;;
 #install_printer  (* univ context future *) ppuniverse_context_future;;
 #install_printer  (* univ context set *) ppuniverse_context_set;;
-#install_printer  (* cumulativity info *) ppcumulativity_info;;
-#install_printer  (* abstract cumulativity info *) ppabstract_cumulativity_info;;
 #install_printer  (* univ set *) ppuniverse_set;;
 #install_printer  (* univ instance *) ppuniverse_instance;;
 #install_printer  (* univ subst *) ppuniverse_subst;;
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 2629cf8626..a3d2f33216 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -222,8 +222,6 @@ let ppuniverseconstraints c = pp (UnivProblem.Set.pr c)
 let ppuniverse_context_future c = 
   let ctx = Future.force c in
     ppuniverse_context ctx
-let ppcumulativity_info c = pp (Univ.pr_cumulativity_info Univ.Level.pr c)
-let ppabstract_cumulativity_info c = pp (Univ.pr_abstract_cumulativity_info Univ.Level.pr c)
 let ppuniverses u = pp (UGraph.pr_universes Level.pr u)
 let ppnamedcontextval e =
   let env = Global.env () in
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index 4d874cdd12..cb32d2294c 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -145,8 +145,6 @@ val ppevar_universe_context : UState.t -> unit
 val ppconstraints : Univ.Constraint.t -> unit
 val ppuniverseconstraints : UnivProblem.Set.t -> unit
 val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit
-val ppcumulativity_info : Univ.CumulativityInfo.t -> unit
-val ppabstract_cumulativity_info : Univ.ACumulativityInfo.t -> unit
 val ppuniverses : UGraph.t -> unit
 
 val ppnamedcontextval : Environ.named_context_val -> unit
-- 
cgit v1.2.3