diff options
author | 2017-12-13 01:38:39 +0100 | |
---|---|---|
committer | 2017-12-15 17:45:55 +0100 | |
commit | 53f5cc210da4debd5264d6d8651a76281b0b4256 (patch) | |
tree | 8e1edbb93c15a88480c8bc4454cc9b8fc15c88c1 /dev/ci | |
parent | c75619228e1c878644edbc49c5cb690777966863 (diff) |
[econstr] Switch constrintern API to non-imperative style.
We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step
desirable to progress with EConstr there.
Diffstat (limited to 'dev/ci')
-rw-r--r-- | dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh b/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh new file mode 100644 index 000000000..8aea7dee3 --- /dev/null +++ b/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh @@ -0,0 +1,4 @@ +if [ "$TRAVIS_PULL_REQUEST" = "6413" ] || [ "$TRAVIS_BRANCH" = "interp+less_impstyle_p2" ]; then + Equations_CI_BRANCH=interp+less_impstyle_p2 + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations.git +fi |