From 325f7ffb27496c8017d50712fe100658ea39bf2b Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 9 Jan 2019 14:01:51 +0100
Subject: [ci] compile with -quick & validate after vio2vo

---
 .gitlab-ci.yml | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index f54f64bf28..413836f956 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -245,6 +245,12 @@ build:base+async:
     COQ_EXTRA_CONF: "-native-compiler yes -coqide opt"
     COQUSERFLAGS: "-async-proofs on"
 
+build:quick:
+  <<: *build-template
+  variables:
+    COQ_EXTRA_CONF: "-native-compiler no"
+    QUICK: "1"
+
 windows64:
   <<: *windows-template
   variables:
@@ -454,6 +460,11 @@ validate:edge+flambda:
     OPAM_SWITCH: edge
     OPAM_VARIANT: "+flambda"
 
+validate:quick:
+  <<: *validate-template
+  dependencies:
+    - build:quick
+
 # Libraries are by convention the projects that depend on Coq
 # but not on its ML API
 
-- 
cgit v1.2.3