vendor/coq-serapi/tests/sertop/full_env.in

+("query0"("Add"()"Require Coq.Vectors.Vector.\nRequire Import Coq.Strings.String Coq.Arith.PeanoNat.\nImport EqNotations Vector.VectorNotations."))
+("query1"("Exec""2"))
+("query2"("Query"(("sid""2"))"EGoals"))
+("query3"("Exec""3"))
+("query4"("Query"(("sid""3"))"EGoals"))
+("query5"("Exec""4"))
+("query6"("Query"(("sid""4"))"EGoals"))
+("query7"("Add"()"Lemma map_snoc_1234 :\n  Vector.map (fun x => 2 * x) (cons 1 [2; 3; 4]) = [2; 4; 6; 8].\nProof.\n  cbv -[Vector.map Nat.mul].\n  Fail destruct (Nat.add_1_r 3). (* .messages *)\nAbort."))
+("query8"("Exec""5"))

webpack.config.js

@@ -128,16 +128,6 @@ export default (env, argv) => [
     rules: [ts, css, imgs, vuesfc],
     unknownContextCritical: false  /* for `randombytes` */
   },
-  optimization: {
-    splitChunks: {
-      cacheGroups: {
-        roninVendor: {
-          /* assume all async-import'ed modules are Ronin; there are too many to list */
-          name: 'ronin-p2p'
-        }
-      }
-    }
-  },
   plugins: shims.plugins
            //[new webpack.ProvidePlugin({process: 'process/browser.js',
            //                            Buffer: ['buffer', 'Buffer']})]