From 788b47d9dd70dc9f8057d4a9353ed24f091ea917 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 20 May 2019 17:02:55 +0200
Subject: Vernacextend only returns a proof_global.t option, not a vernacstate

---
 dev/top_printers.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 2859b56cbe..db444a9b78 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -532,7 +532,7 @@ let _ =
   let open Vernacextend in
   let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in
   let cmd_sig = TyTerminal("PrintConstr", TyNonTerminal(ty_constr, TyNil)) in
-  let cmd_fn c ~atts ~st = in_current_context econstr_display c; st in
+  let cmd_fn c ~atts ~pstate = in_current_context econstr_display c; pstate in
   let cmd_class _ = VtQuery,VtNow in
   let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in
   vernac_extend ~command:"PrintConstr" [cmd]
@@ -541,7 +541,7 @@ let _ =
   let open Vernacextend in
   let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in
   let cmd_sig = TyTerminal("PrintPureConstr", TyNonTerminal(ty_constr, TyNil)) in
-  let cmd_fn c ~atts ~st = in_current_context print_pure_econstr c; st in
+  let cmd_fn c ~atts ~pstate = in_current_context print_pure_econstr c; pstate in
   let cmd_class _ = VtQuery,VtNow in
   let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in
   vernac_extend ~command:"PrintPureConstr" [cmd]
-- 
cgit v1.2.3


From 96231a23a9b76b17541572defb6089e23e80c474 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 6 May 2019 14:02:53 +0200
Subject: Overlays for coq/coq#10050 (proof_global API changes)

---
 .../user-overlays/10050-SkySkimmer-pass-less-ontop.sh  | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 dev/ci/user-overlays/10050-SkySkimmer-pass-less-ontop.sh

(limited to 'dev')

diff --git a/dev/ci/user-overlays/10050-SkySkimmer-pass-less-ontop.sh b/dev/ci/user-overlays/10050-SkySkimmer-pass-less-ontop.sh
new file mode 100644
index 0000000000..0c3f1eefed
--- /dev/null
+++ b/dev/ci/user-overlays/10050-SkySkimmer-pass-less-ontop.sh
@@ -0,0 +1,18 @@
+if [ "$CI_PULL_REQUEST" = "10050" ] || [ "$CI_BRANCH" = "pass-less-ontop" ]; then
+
+    elpi_CI_REF=pass-less-ontop
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+    equations_CI_REF=pass-less-ontop
+    equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+    mtac2_CI_REF=pass-less-ontop
+    mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2
+
+    paramcoq_CI_REF=pass-less-ontop
+    paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
+
+    quickchick_CI_REF=pass-less-ontop
+    quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick
+
+fi
-- 
cgit v1.2.3


From 3b7509b96273f4e412b747e0c55dd193f38fd418 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 21 May 2019 23:06:40 +0200
Subject: VernacExtend produces vernac_interp_phase ADT (old name
 functional_vernac)

+ hide interp_functional_vernac in vernacentries
---
 dev/top_printers.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index db444a9b78..4ce87faaa1 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -532,7 +532,7 @@ let _ =
   let open Vernacextend in
   let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in
   let cmd_sig = TyTerminal("PrintConstr", TyNonTerminal(ty_constr, TyNil)) in
-  let cmd_fn c ~atts ~pstate = in_current_context econstr_display c; pstate in
+  let cmd_fn c ~atts = VtDefault (fun () -> in_current_context econstr_display c) in
   let cmd_class _ = VtQuery,VtNow in
   let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in
   vernac_extend ~command:"PrintConstr" [cmd]
@@ -541,7 +541,7 @@ let _ =
   let open Vernacextend in
   let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in
   let cmd_sig = TyTerminal("PrintPureConstr", TyNonTerminal(ty_constr, TyNil)) in
-  let cmd_fn c ~atts ~pstate = in_current_context print_pure_econstr c; pstate in
+  let cmd_fn c ~atts = VtDefault (fun () -> in_current_context print_pure_econstr c) in
   let cmd_class _ = VtQuery,VtNow in
   let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in
   vernac_extend ~command:"PrintPureConstr" [cmd]
-- 
cgit v1.2.3


From 13915784a568f9e0c8a15c99a516a898726dbc61 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 27 May 2019 16:40:52 +0200
Subject: update overlays

---
 .../user-overlays/10050-SkySkimmer-pass-less-ontop.sh  | 18 ------------------
 dev/ci/user-overlays/10215-gares-less-ontop.sh         | 15 +++++++++++++++
 2 files changed, 15 insertions(+), 18 deletions(-)
 delete mode 100644 dev/ci/user-overlays/10050-SkySkimmer-pass-less-ontop.sh
 create mode 100644 dev/ci/user-overlays/10215-gares-less-ontop.sh

(limited to 'dev')

diff --git a/dev/ci/user-overlays/10050-SkySkimmer-pass-less-ontop.sh b/dev/ci/user-overlays/10050-SkySkimmer-pass-less-ontop.sh
deleted file mode 100644
index 0c3f1eefed..0000000000
--- a/dev/ci/user-overlays/10050-SkySkimmer-pass-less-ontop.sh
+++ /dev/null
@@ -1,18 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "10050" ] || [ "$CI_BRANCH" = "pass-less-ontop" ]; then
-
-    elpi_CI_REF=pass-less-ontop
-    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
-
-    equations_CI_REF=pass-less-ontop
-    equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
-
-    mtac2_CI_REF=pass-less-ontop
-    mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2
-
-    paramcoq_CI_REF=pass-less-ontop
-    paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
-
-    quickchick_CI_REF=pass-less-ontop
-    quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick
-
-fi
diff --git a/dev/ci/user-overlays/10215-gares-less-ontop.sh b/dev/ci/user-overlays/10215-gares-less-ontop.sh
new file mode 100644
index 0000000000..bceb5ad0e8
--- /dev/null
+++ b/dev/ci/user-overlays/10215-gares-less-ontop.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "10215" ] || [ "$CI_BRANCH" = "custom-typing" ]; then
+
+    equations_CI_REF=pass-less-ontop
+    equations_CI_GITURL=https://github.com/gares/Coq-Equations
+
+    mtac2_CI_REF=pass-less-ontop
+    mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2
+
+    paramcoq_CI_REF=pass-less-ontop
+    paramcoq_CI_GITURL=https://github.com/gares/paramcoq
+
+    quickchick_CI_REF=pass-less-ontop
+    quickchick_CI_GITURL=https://github.com/gares/QuickChick
+
+fi
-- 
cgit v1.2.3