/usr/share/doc/libaac-tactics-ocaml-dev/html/api/Coq.html is in libaac-tactics-ocaml-dev 8.6.1-1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 | <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<link rel="stylesheet" href="style.css" type="text/css">
<meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type">
<link rel="Start" href="index.html">
<link rel="previous" href="Aac_rewrite.html">
<link rel="next" href="Helper.html">
<link rel="Up" href="index.html">
<link title="Index of types" rel=Appendix href="index_types.html">
<link title="Index of values" rel=Appendix href="index_values.html">
<link title="Index of modules" rel=Appendix href="index_modules.html">
<link title="Index of module types" rel=Appendix href="index_module_types.html">
<link title="Aac_rewrite" rel="Chapter" href="Aac_rewrite.html">
<link title="Coq" rel="Chapter" href="Coq.html">
<link title="Helper" rel="Chapter" href="Helper.html">
<link title="Matcher" rel="Chapter" href="Matcher.html">
<link title="Print" rel="Chapter" href="Print.html">
<link title="Search_monad" rel="Chapter" href="Search_monad.html">
<link title="Theory" rel="Chapter" href="Theory.html"><link title="Getting Coq terms from the environment" rel="Section" href="#2_GettingCoqtermsfromtheenvironment">
<link title="General purpose functions" rel="Section" href="#2_Generalpurposefunctions">
<link title="Bindings with Coq' Standard Library" rel="Section" href="#2_BindingswithCoqStandardLibrary">
<link title="Some tacticials" rel="Section" href="#2_Sometacticials">
<link title="Error related mechanisms" rel="Section" href="#2_Errorrelatedmechanisms">
<link title="Rewriting tactics used in aac_rewrite" rel="Section" href="#2_Rewritingtacticsusedinaacrewrite">
<title>Coq</title>
</head>
<body>
<div class="navbar"><a class="pre" href="Aac_rewrite.html" title="Aac_rewrite">Previous</a>
<a class="up" href="index.html" title="Index">Up</a>
<a class="post" href="Helper.html" title="Helper">Next</a>
</div>
<h1>Module <a href="type_Coq.html">Coq</a></h1>
<pre><span class="keyword">module</span> Coq: <code class="code">sig</code> <a href="Coq.html">..</a> <code class="code">end</code></pre><div class="info module top">
Interface with Coq where we define some handlers for Coq's API,
and we import several definitions from Coq's standard library.
<p>
This general purpose library could be reused by other plugins.
<p>
Some salient points:<ul>
<li>we use Caml's module system to mimic Coq's one, and avoid cluttering
the namespace;</li>
<li>we also provide several handlers for standard coq tactics, in
order to provide a unified setting (we replace functions that
modify the evar_map by functions that operate on the whole
goal, and repack the modified evar_map with it).</li>
</ul>
<br>
</div>
<hr width="100%">
<br>
<h2 id="2_GettingCoqtermsfromtheenvironment">Getting Coq terms from the environment</h2><br>
<pre><span id="VALinit_constant"><span class="keyword">val</span> init_constant</span> : <code class="type">string list -> string -> Term.constr</code></pre><br>
<h2 id="2_Generalpurposefunctions">General purpose functions</h2><br>
<pre><span id="TYPEgoal_sigma"><span class="keyword">type</span> <code class="type"></code>goal_sigma</span> = <code class="type">Proof_type.goal Tacmach.sigma</code> </pre>
<pre><span id="VALgoal_update"><span class="keyword">val</span> goal_update</span> : <code class="type"><a href="Coq.html#TYPEgoal_sigma">goal_sigma</a> -> Evd.evar_map -> <a href="Coq.html#TYPEgoal_sigma">goal_sigma</a></code></pre>
<pre><span id="VALresolve_one_typeclass"><span class="keyword">val</span> resolve_one_typeclass</span> : <code class="type">Proof_type.goal Tacmach.sigma -> Term.types -> Term.constr * <a href="Coq.html#TYPEgoal_sigma">goal_sigma</a></code></pre>
<pre><span id="VALcps_resolve_one_typeclass"><span class="keyword">val</span> cps_resolve_one_typeclass</span> : <code class="type">?error:string -><br> Term.types -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic</code></pre>
<pre><span id="VALnf_evar"><span class="keyword">val</span> nf_evar</span> : <code class="type"><a href="Coq.html#TYPEgoal_sigma">goal_sigma</a> -> Term.constr -> Term.constr</code></pre>
<pre><span id="VALfresh_evar"><span class="keyword">val</span> fresh_evar</span> : <code class="type"><a href="Coq.html#TYPEgoal_sigma">goal_sigma</a> -> Term.types -> Term.constr * <a href="Coq.html#TYPEgoal_sigma">goal_sigma</a></code></pre>
<pre><span id="VALevar_unit"><span class="keyword">val</span> evar_unit</span> : <code class="type"><a href="Coq.html#TYPEgoal_sigma">goal_sigma</a> -> Term.constr -> Term.constr * <a href="Coq.html#TYPEgoal_sigma">goal_sigma</a></code></pre>
<pre><span id="VALevar_binary"><span class="keyword">val</span> evar_binary</span> : <code class="type"><a href="Coq.html#TYPEgoal_sigma">goal_sigma</a> -> Term.constr -> Term.constr * <a href="Coq.html#TYPEgoal_sigma">goal_sigma</a></code></pre>
<pre><span id="VALevar_relation"><span class="keyword">val</span> evar_relation</span> : <code class="type"><a href="Coq.html#TYPEgoal_sigma">goal_sigma</a> -> Term.constr -> Term.constr * <a href="Coq.html#TYPEgoal_sigma">goal_sigma</a></code></pre>
<pre><span id="VALcps_evar_relation"><span class="keyword">val</span> cps_evar_relation</span> : <code class="type">Term.constr -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic</code></pre><div class="info ">
<code class="code">cps_mk_letin name v</code> binds the constr <code class="code">v</code> using a letin tactic<br>
</div>
<pre><span id="VALcps_mk_letin"><span class="keyword">val</span> cps_mk_letin</span> : <code class="type">string -><br> Term.constr -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic</code></pre>
<pre><span id="VALretype"><span class="keyword">val</span> retype</span> : <code class="type">Term.constr -> Proof_type.tactic</code></pre>
<pre><span id="VALdecomp_term"><span class="keyword">val</span> decomp_term</span> : <code class="type">Term.constr -> (Term.constr, Term.types) Term.kind_of_term</code></pre>
<pre><span id="VALlapp"><span class="keyword">val</span> lapp</span> : <code class="type">Term.constr lazy_t -> Term.constr array -> Term.constr</code></pre><br>
<h2 id="2_BindingswithCoqStandardLibrary">Bindings with Coq' Standard Library</h2><br>
<pre><span class="keyword">module</span> <a href="Coq.List.html">List</a>: <code class="code">sig</code> <a href="Coq.List.html">..</a> <code class="code">end</code></pre><div class="info">
Coq lists
</div>
<pre><span class="keyword">module</span> <a href="Coq.Pair.html">Pair</a>: <code class="code">sig</code> <a href="Coq.Pair.html">..</a> <code class="code">end</code></pre><div class="info">
Coq pairs
</div>
<pre><span class="keyword">module</span> <a href="Coq.Bool.html">Bool</a>: <code class="code">sig</code> <a href="Coq.Bool.html">..</a> <code class="code">end</code></pre>
<pre><span class="keyword">module</span> <a href="Coq.Comparison.html">Comparison</a>: <code class="code">sig</code> <a href="Coq.Comparison.html">..</a> <code class="code">end</code></pre>
<pre><span class="keyword">module</span> <a href="Coq.Leibniz.html">Leibniz</a>: <code class="code">sig</code> <a href="Coq.Leibniz.html">..</a> <code class="code">end</code></pre>
<pre><span class="keyword">module</span> <a href="Coq.Option.html">Option</a>: <code class="code">sig</code> <a href="Coq.Option.html">..</a> <code class="code">end</code></pre>
<pre><span class="keyword">module</span> <a href="Coq.Pos.html">Pos</a>: <code class="code">sig</code> <a href="Coq.Pos.html">..</a> <code class="code">end</code></pre><div class="info">
Coq positive numbers (pos)
</div>
<pre><span class="keyword">module</span> <a href="Coq.Nat.html">Nat</a>: <code class="code">sig</code> <a href="Coq.Nat.html">..</a> <code class="code">end</code></pre><div class="info">
Coq unary numbers (peano)
</div>
<pre><span class="keyword">module</span> <a href="Coq.Classes.html">Classes</a>: <code class="code">sig</code> <a href="Coq.Classes.html">..</a> <code class="code">end</code></pre><div class="info">
Coq typeclasses
</div>
<pre><span class="keyword">module</span> <a href="Coq.Relation.html">Relation</a>: <code class="code">sig</code> <a href="Coq.Relation.html">..</a> <code class="code">end</code></pre>
<pre><span class="keyword">module</span> <a href="Coq.Transitive.html">Transitive</a>: <code class="code">sig</code> <a href="Coq.Transitive.html">..</a> <code class="code">end</code></pre>
<pre><span class="keyword">module</span> <a href="Coq.Equivalence.html">Equivalence</a>: <code class="code">sig</code> <a href="Coq.Equivalence.html">..</a> <code class="code">end</code></pre>
<pre><span id="VALmatch_as_equation"><span class="keyword">val</span> match_as_equation</span> : <code class="type">?context:Context.Rel.t -><br> <a href="Coq.html#TYPEgoal_sigma">goal_sigma</a> -><br> Term.constr -> (Term.constr * Term.constr * <a href="Coq.Relation.html#TYPEt">Relation.t</a>) option</code></pre><div class="info ">
<code class="code">match_as_equation ?context goal c</code> try to decompose c as a
relation applied to two terms. An optionnal rel-context can be
provided to ensure that the term remains typable<br>
</div>
<br>
<h2 id="2_Sometacticials">Some tacticials</h2><br>
<pre><span id="VALtclTIME"><span class="keyword">val</span> tclTIME</span> : <code class="type">string -> Proof_type.tactic -> Proof_type.tactic</code></pre><div class="info ">
time the execution of a tactic<br>
</div>
<pre><span id="VALtclDEBUG"><span class="keyword">val</span> tclDEBUG</span> : <code class="type">string -> Proof_type.tactic -> Proof_type.tactic</code></pre><div class="info ">
emit debug messages to see which tactics are failing<br>
</div>
<pre><span id="VALtclPRINT"><span class="keyword">val</span> tclPRINT</span> : <code class="type">Proof_type.tactic -> Proof_type.tactic</code></pre><div class="info ">
print the current goal<br>
</div>
<br>
<h2 id="2_Errorrelatedmechanisms">Error related mechanisms</h2><br>
<pre><span id="VALanomaly"><span class="keyword">val</span> anomaly</span> : <code class="type">string -> 'a</code></pre>
<pre><span id="VALuser_error"><span class="keyword">val</span> user_error</span> : <code class="type">string -> 'a</code></pre>
<pre><span id="VALwarning"><span class="keyword">val</span> warning</span> : <code class="type">string -> unit</code></pre><br>
<h2 id="2_Rewritingtacticsusedinaacrewrite">Rewriting tactics used in aac_rewrite</h2><br>
<pre><span class="keyword">module</span> <a href="Coq.Rewrite.html">Rewrite</a>: <code class="code">sig</code> <a href="Coq.Rewrite.html">..</a> <code class="code">end</code></pre></body></html>
|