diff options
| author | Emilio Jesus Gallego Arias | 2019-09-03 16:42:53 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-09-18 16:16:08 +0200 |
| commit | cca4665778dd799e5802594761e13b8d53502824 (patch) | |
| tree | 38105676715268d8d3fcaf4b0cb98caf3d5c8ed1 /dev | |
| parent | 42ff3109217452853c3b853d21f09a317dd6e37d (diff) | |
[declaremods] Remove abstraction layer over module interpretation.
Now that we place imperative module declaration on top of module
interpretation we can remove the abstraction layer used in
`Declaremods`, so the `interp_modast` parameter goes away.
Improvement suggested by Gaëtan Gilbert.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh b/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh new file mode 100644 index 0000000000..a5f6551474 --- /dev/null +++ b/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10727" ] || [ "$CI_BRANCH" = "library+to_vernac_step2" ]; then + + elpi_CI_REF=library+to_vernac_step2 + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + +fi |