<!DOCTYPE html>
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>elpi: 3 m 17 s 🏆</title>
    <link rel="shortcut icon" type="image/png" href="../../../../../favicon.png" />
    <link href="../../../../../bootstrap.min.css" rel="stylesheet">
    <link href="../../../../../bootstrap-custom.css" rel="stylesheet">
    <link href="//maxcdn.bootstrapcdn.com/font-awesome/4.2.0/css/font-awesome.min.css" rel="stylesheet">
    <script src="../../../../../moment.min.js"></script>
    <!-- HTML5 Shim and Respond.js IE8 support of HTML5 elements and media queries -->
    <!-- WARNING: Respond.js doesn't work if you view the page via file:// -->
    <!--[if lt IE 9]>
      <script src="https://oss.maxcdn.com/html5shiv/3.7.2/html5shiv.min.js"></script>
      <script src="https://oss.maxcdn.com/respond/1.4.2/respond.min.js"></script>
    <![endif]-->
  </head>
  <body>
    <div class="container">
      <div class="navbar navbar-default" role="navigation">
        <div class="container-fluid">
          <div class="navbar-header">
            <a class="navbar-brand" href="../../../../.."><i class="fa fa-lg fa-flag-checkered"></i> Coq bench</a>
          </div>
          <div id="navbar" class="collapse navbar-collapse">
            <ul class="nav navbar-nav">
              <li><a href="../..">clean / released</a></li>
              <li class="active"><a href="">8.11.2 / elpi - 1.3.1</a></li>
            </ul>
          </div>
        </div>
      </div>
      <div class="article">
        <div class="row">
          <div class="col-md-12">
            <a href="../..">« Up</a>
            <h1>
              elpi
              <small>
                1.3.1
                <span class="label label-success">3 m 17 s 🏆</span>
              </small>
            </h1>
            <p>📅 <em><script>document.write(moment("2021-11-01 03:33:26 +0000", "YYYY-MM-DD HH:mm:ss Z").fromNow());</script> (2021-11-01 03:33:26 UTC)</em><p>
            <h2>Context</h2>
            <pre># Packages matching: installed
# Name              # Installed # Synopsis
base-bigarray       base
base-threads        base
base-unix           base
conf-findutils      1           Virtual package relying on findutils
coq                 8.11.2      Formal proof management system
num                 1.4         The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.09.1      The OCaml compiler (virtual package)
ocaml-base-compiler 4.09.1      Official release 4.09.1
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.9.1       A library manager for OCaml
# opam file:
opam-version: &quot;2.0&quot;
maintainer: &quot;Enrico Tassi &lt;enrico.tassi@inria.fr&gt;&quot;
authors: [ &quot;Enrico Tassi&quot; ]
license: &quot;LGPL-2.1-or-later&quot;
homepage: &quot;https://github.com/LPCIC/coq-elpi&quot;
bug-reports: &quot;https://github.com/LPCIC/coq-elpi/issues&quot;
dev-repo: &quot;git+https://github.com/LPCIC/coq-elpi&quot;
build: [ make &quot;COQBIN=%{bin}%/&quot; &quot;ELPIDIR=%{prefix}%/lib/elpi&quot; ]
install: [ make &quot;install&quot; &quot;COQBIN=%{bin}%/&quot; &quot;ELPIDIR=%{prefix}%/lib/elpi&quot; ]
depends: [
  &quot;elpi&quot; {&gt;= &quot;1.10.2&quot; &amp; &lt; &quot;1.11.0~&quot;}
  &quot;coq&quot; {&gt;= &quot;8.11&quot; &amp; &lt; &quot;8.12~&quot;}
  ]
synopsis: &quot;Elpi extension language for Coq&quot;
description: &quot;&quot;&quot;
Coq-elpi provides a Coq plugin that embeds ELPI.
It also provides a way to embed Coq&#39;s terms into λProlog using
the Higher-Order Abstract Syntax approach
and a way to read terms back.  In addition to that it exports to ELPI a
set of Coq&#39;s primitives, e.g. printing a message, accessing the
environment of theorems and data types, defining a new constant and so on.
For convenience it also provides a quotation and anti-quotation for Coq&#39;s
syntax in λProlog.  E.g. `{{nat}}` is expanded to the type name of natural
numbers, or `{{A -&gt; B}}` to the representation of a product by unfolding
the `-&gt;` notation. Finally it provides a way to define new vernacular commands
and new tactics.&quot;&quot;&quot;
url {
src: &quot;https://github.com/LPCIC/coq-elpi/archive/v1.3.1.tar.gz&quot;
checksum: &quot;sha256=d4ef1c2dcd0b7c5081998089ce9a908a99bab339701ebb65afa5a24865751e79&quot;
}
</pre>
            <h2>Lint</h2>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>true</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
            </dl>
            <h2>Dry install 🏜️</h2>
            <p>Dry install with the current Coq version:</p>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>opam install -y --show-action coq-elpi.1.3.1 coq.8.11.2</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
            </dl>
            <p>Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:</p>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>true</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
            </dl>
            <h2>Install dependencies</h2>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-elpi.1.3.1 coq.8.11.2</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Duration</dt>
              <dd>6 m 53 s</dd>
            </dl>
            <h2>Install 🚀</h2>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-elpi.1.3.1 coq.8.11.2</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Duration</dt>
              <dd>3 m 17 s</dd>
            </dl>
            <h2>Installation size</h2>
            <p>Total: 26 M</p>
            <ul>
              <li>6 M <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/elpi_plugin.cma</code></li>
              <li>6 M <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/elpi_plugin.cmxs</code></li>
              <li>3 M <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_projK.vo</code></li>
              <li>2 M <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_derive.vo</code></li>
              <li>2 M <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/elpi_plugin.cmo</code></li>
              <li>905 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_param1.vo</code></li>
              <li>439 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_param2.vo</code></li>
              <li>423 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_bcongr.vo</code></li>
              <li>381 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/examples/example_usage_derive.vo</code></li>
              <li>337 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_eqK.vo</code></li>
              <li>313 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive.vo</code></li>
              <li>252 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_isK.vo</code></li>
              <li>174 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/elpi.vo</code></li>
              <li>167 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/examples/example_reflexive_tactic.vo</code></li>
              <li>165 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tutorial/coq_elpi.vo</code></li>
              <li>137 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tests/test_tactic.vo</code></li>
              <li>125 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tests/test_HOAS.vo</code></li>
              <li>119 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/examples/example_data_base.vo</code></li>
              <li>117 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_eq.vo</code></li>
              <li>117 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tests/test_elaborator.vo</code></li>
              <li>106 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_induction.vo</code></li>
              <li>105 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tests/test_API.vo</code></li>
              <li>103 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/cast.vo</code></li>
              <li>103 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_param1_functor.vo</code></li>
              <li>102 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/induction.vo</code></li>
              <li>101 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_eqOK.vo</code></li>
              <li>97 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/param1_inhab.vo</code></li>
              <li>97 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/param1_trivial.vo</code></li>
              <li>97 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_idx2inv.vo</code></li>
              <li>91 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/elpi_plugin.cmx</code></li>
              <li>90 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/param2.vo</code></li>
              <li>89 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/eqOK.vo</code></li>
              <li>87 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/examples/example_record_expansion.vo</code></li>
              <li>87 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/param1.vo</code></li>
              <li>81 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tutorial/elpi_lang.vo</code></li>
              <li>81 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/examples/example_curry_howard_tactics.vo</code></li>
              <li>80 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/bcongr.vo</code></li>
              <li>80 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/ltac/tests/test_ltac.vo</code></li>
              <li>78 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/param1_congr.vo</code></li>
              <li>78 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/param1_functor.vo</code></li>
              <li>77 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_map.vo</code></li>
              <li>76 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/eqK.vo</code></li>
              <li>76 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_param1_inhab.vo</code></li>
              <li>75 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/map.vo</code></li>
              <li>74 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/projK.vo</code></li>
              <li>74 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tests/test_vernacular1.vo</code></li>
              <li>74 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/ltac/injection.vo</code></li>
              <li>74 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_param1_congr.vo</code></li>
              <li>74 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/eq.vo</code></li>
              <li>72 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/eqcorrect.vo</code></li>
              <li>71 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/ltac/discriminate.vo</code></li>
              <li>70 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/invert.vo</code></li>
              <li>70 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/examples/example_fuzzer.vo</code></li>
              <li>69 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/wip/memoization.vo</code></li>
              <li>66 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/idx2inv.vo</code></li>
              <li>64 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tests/test_quotation.vo</code></li>
              <li>64 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/isK.vo</code></li>
              <li>61 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_eqcorrect.vo</code></li>
              <li>59 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_param1_trivial.vo</code></li>
              <li>58 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/elpi_plugin.cmi</code></li>
              <li>50 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_derive_stdlib.vo</code></li>
              <li>49 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/ltac/tests/test_injection.vo</code></li>
              <li>45 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/examples/example_reflexive_tactic.glob</code></li>
              <li>33 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/coq-builtin.elpi</code></li>
              <li>31 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_derive_stdlib.glob</code></li>
              <li>29 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tutorial/elpi_lang.v</code></li>
              <li>23 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/ltac/tests/test_discriminate.vo</code></li>
              <li>23 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_invert.vo</code></li>
              <li>23 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tutorial/coq_elpi.v</code></li>
              <li>23 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_derive.glob</code></li>
              <li>16 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_induction.glob</code></li>
              <li>14 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/coq-lib.elpi</code></li>
              <li>14 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tests/test_API.v</code></li>
              <li>13 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_projK.glob</code></li>
              <li>13 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_bcongr.glob</code></li>
              <li>12 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_param1.glob</code></li>
              <li>12 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_param1_congr.glob</code></li>
              <li>12 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/coq-HOAS.elpi</code></li>
              <li>11 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tests/test_API.glob</code></li>
              <li>10 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/elpi_plugin.cmxa</code></li>
              <li>9 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/examples/example_reflexive_tactic.v</code></li>
              <li>9 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/examples/example_record_expansion.v</code></li>
              <li>8 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/examples/example_fuzzer.glob</code></li>
              <li>8 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_eqK.glob</code></li>
              <li>8 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_param1_functor.glob</code></li>
              <li>7 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_param2.glob</code></li>
              <li>6 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_param1_trivial.glob</code></li>
              <li>6 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_eqOK.glob</code></li>
              <li>6 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_param1_inhab.glob</code></li>
              <li>6 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_eqcorrect.glob</code></li>
              <li>5 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_eq.glob</code></li>
              <li>5 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_idx2inv.v</code></li>
              <li>5 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_isK.glob</code></li>
              <li>5 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_derive_stdlib.v</code></li>
              <li>5 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/elpi.glob</code></li>
              <li>5 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive.glob</code></li>
              <li>5 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_map.glob</code></li>
              <li>4 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tests/test_elaborator.glob</code></li>
              <li>4 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tutorial/coq_elpi.glob</code></li>
              <li>4 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_derive.v</code></li>
              <li>4 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/ltac/tests/test_discriminate.glob</code></li>
              <li>4 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/coq-lib-extra.elpi</code></li>
              <li>4 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_invert.glob</code></li>
              <li>4 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tests/test_elaborator.v</code></li>
              <li>4 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_param1.v</code></li>
              <li>3 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tests/test_tactic.glob</code></li>
              <li>3 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tests/test_tactic.v</code></li>
              <li>3 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/examples/example_fuzzer.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_param2.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_induction.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/examples/example_record_expansion.glob</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/ltac/tests/test_injection.glob</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/examples/example_data_base.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/elpi.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_bcongr.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_idx2inv.glob</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_eqOK.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_param1_congr.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_projK.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/examples/example_curry_howard_tactics.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tests/test_HOAS.glob</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/examples/example_curry_howard_tactics.glob</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_eqcorrect.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_param1_trivial.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/wip/memoization.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_eqK.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tests/test_HOAS.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/wip/memoization.glob</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/param1_trivial.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_param1_functor.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_param1_inhab.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tests/test_vernacular2.vo</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/param1_inhab.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tests/test_quotation.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/param2.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/param1.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_isK.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/ltac/tests/test_ltac.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tests/test_quotation.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/examples/example_usage_derive.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/eqcorrect.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_eq.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/examples/example_usage_derive.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tests/test_vernacular1.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_map.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/induction.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/eqK.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/eqOK.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/param1_congr.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/bcongr.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/eq.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/projK.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/param1_trivial.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/ltac/tests/test_ltac.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/param1_functor.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/eqcorrect.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/isK.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/map.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/bcongr.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/idx2inv.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/eqK.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/invert.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/eq.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/ltac/tests/test_discriminate.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/param2.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/ltac/tests/test_injection.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/cast.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/tests/test_invert.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/param1_congr.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/ltac/injection.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/param1.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/ltac/discriminate.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/eqOK.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/param1_inhab.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/ltac/discriminate.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/induction.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tests/test_vernacular1.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/isK.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/projK.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/ltac/injection.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/invert.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/param1_functor.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/idx2inv.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/cast.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tests/test_vernacular2.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/examples/example_data_base.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tests/test_vernacular2.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/tutorial/elpi_lang.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/elpi/derive/map.glob</code></li>
            </ul>
            <h2>Uninstall 🧹</h2>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>opam remove -y coq-elpi.1.3.1</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Missing removes</dt>
              <dd>
                none
              </dd>
              <dt>Wrong removes</dt>
              <dd>
                none
              </dd>
            </dl>
          </div>
        </div>
      </div>
      <hr/>
      <div class="footer">
        <p class="text-center">
          Sources are on <a href="https://github.com/coq-bench">GitHub</a> © Guillaume Claret 🐣
        </p>
      </div>
    </div>
    <script src="https://ajax.googleapis.com/ajax/libs/jquery/1.11.1/jquery.min.js"></script>
    <script src="../../../../../bootstrap.min.js"></script>
  </body>
</html>
