aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-08-18 20:27:52 +0200
committerEmilio Jesus Gallego Arias2019-08-19 23:03:45 +0200
commita74e055acf48583c6fece5d22c805736679376b2 (patch)
treebc86b65608590013d7569b9585cd37029f2fa274 /dev
parent7f9a08b98b1637291dda687fce92198a21ffc395 (diff)
[api] Move handling of variable implicit data to impargs
We move `binder_kind` to the pretyping AST, removing the last data type in the now orphaned file `Decl_kinds`. This seems a better fit, as this data is not relevant to the lower layers but only used in `Impargs`. We also move state keeping to `Impargs`, so now implicit declaration must include the type. We also remove a duplicated function.
Diffstat (limited to 'dev')
-rw-r--r--dev/ci/user-overlays/10665-ejgallego-api+varkind.sh9
1 files changed, 9 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/10665-ejgallego-api+varkind.sh b/dev/ci/user-overlays/10665-ejgallego-api+varkind.sh
new file mode 100644
index 0000000000..0c47f6a60b
--- /dev/null
+++ b/dev/ci/user-overlays/10665-ejgallego-api+varkind.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "10665" ] || [ "$CI_BRANCH" = "api+varkind" ]; then
+
+ elpi_CI_REF=api+varkind
+ elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+ quickchick_CI_REF=api+varkind
+ quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick
+
+fi