htmldoc regenerated

1 files changed, 107 insertions, 0 deletions

diff --git a/docs/htmldoc/mathcomp.ssreflect.ssreflect.html b/docs/htmldoc/mathcomp.ssreflect.ssreflect.html
index db045f6..7772d24 100644
--- a/docs/htmldoc/mathcomp.ssreflect.ssreflect.html
+++ b/docs/htmldoc/mathcomp.ssreflect.ssreflect.html
@@ -24,6 +24,113 @@
 
 <br/>
 </div>
+
+<div class="doc">
+ Local additions:                                                           
+   nonPropType == an interface for non-Prop Types: a nonPropType coerces    
+                  to a Type, and only types that do <i>not</i> have sort         
+                  Prop are canonical nonPropType instances. This is         
+                  useful for applied views.                                 
+&gt; This will become standard with the Coq v8.11 SSReflect core library. 
+  deprecate old new == new, but warning that old is deprecated and new      
+                       should be used instead.                              
+&gt; Usage: Notation old := (deprecate old new) (only parsing).          
+&gt; Caveat: deprecate old new only inherits new's maximal implicits;    
+        on-demand implicits should be added after : (deprecate old new _).  
+&gt; Caveat 2: if premises or conclusions need to be adjusted, of for    
+        non-prenex implicits, use the idiom:                                
+         Notation old := ((fun a1 a2 ... =&gt; deprecate old new a1 a2 ...)    
+                          _  ... _) (only printing).                       
+        where all the implicit a_i's occur first, and correspond to the     
+        trailing <i>'s, making sure deprecate old new is fully applied and    
+        there are <i>no implicits</i> inside the (fun .. =&gt; ..) expression. This 
+        is to avoid triggering a bug in SSReflect elaboration that is       
+        triggered by such evars under binders.                              
+  Import Deprecation.Silent :: turn off deprecation warning messages.       
+  Import Deprecation.Reject :: raise an error instead of only warning.       
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Module</span> <a name="NonPropType"><span class="id" title="module">NonPropType</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Structure</span> <a name="NonPropType.call_of"><span class="id" title="record">call_of</span></a> (<span class="id" title="var">condition</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a>) (<span class="id" title="var">result</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>) := <a name="NonPropType.Call"><span class="id" title="constructor">Call</span></a> {<a name="NonPropType.callee"><span class="id" title="projection">callee</span></a> : <span class="id" title="keyword">Type</span>}.<br/>
+<span class="id" title="keyword">Definition</span> <a name="NonPropType.maybeProp"><span class="id" title="definition">maybeProp</span></a> (<span class="id" title="var">T</span> : <span class="id" title="keyword">Type</span>) := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#tt"><span class="id" title="constructor">tt</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="NonPropType.call"><span class="id" title="definition">call</span></a> <span class="id" title="var">T</span> := <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.Call"><span class="id" title="constructor">Call</span></a> (<a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.maybeProp"><span class="id" title="definition">maybeProp</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#T"><span class="id" title="variable">T</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#T"><span class="id" title="variable">T</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Structure</span> <a name="NonPropType.test_of"><span class="id" title="record">test_of</span></a> (<span class="id" title="var">result</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>) := <a name="NonPropType.Test"><span class="id" title="constructor">Test</span></a> {<a name="NonPropType.condition"><span class="id" title="projection">condition</span></a> :&gt; <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a>}.<br/>
+<span class="id" title="keyword">Definition</span> <a name="NonPropType.test_Prop"><span class="id" title="definition">test_Prop</span></a> (<span class="id" title="var">P</span> : <span class="id" title="keyword">Prop</span>) := <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.Test"><span class="id" title="constructor">Test</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a> (<a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.maybeProp"><span class="id" title="definition">maybeProp</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#P"><span class="id" title="variable">P</span></a>).<br/>
+<span class="id" title="keyword">Definition</span> <a name="NonPropType.test_negative"><span class="id" title="definition">test_negative</span></a> := <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.Test"><span class="id" title="constructor">Test</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#tt"><span class="id" title="constructor">tt</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Structure</span> <a name="NonPropType.type"><span class="id" title="record">type</span></a> :=<br/>
+&nbsp;&nbsp;<a name="NonPropType.Check"><span class="id" title="constructor">Check</span></a> {<a name="NonPropType.result"><span class="id" title="projection">result</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>; <a name="NonPropType.test"><span class="id" title="projection">test</span></a> : <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.test_of"><span class="id" title="record">test_of</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#result"><span class="id" title="method">result</span></a>; <a name="NonPropType.frame"><span class="id" title="projection">frame</span></a> : <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.call_of"><span class="id" title="record">call_of</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#test"><span class="id" title="method">test</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#result"><span class="id" title="method">result</span></a>}.<br/>
+<span class="id" title="keyword">Definition</span> <a name="NonPropType.check"><span class="id" title="definition">check</span></a> <span class="id" title="var">result</span> <span class="id" title="var">test</span> <span class="id" title="var">frame</span> := @<a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.Check"><span class="id" title="constructor">Check</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#result"><span class="id" title="variable">result</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#test"><span class="id" title="variable">test</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#frame"><span class="id" title="variable">frame</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Module</span> <a name="NonPropType.Exports"><span class="id" title="module">Exports</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">call</span>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">test_Prop</span>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">test_negative</span>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">check</span>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="NonPropType.Exports.nonPropType"><span class="id" title="abbreviation">nonPropType</span></a> := <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.type"><span class="id" title="record">type</span></a>.<br/>
+<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.callee"><span class="id" title="projection">callee</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.callee"><span class="id" title="projection">:</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.callee"><span class="id" title="projection">call_of</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.callee"><span class="id" title="projection">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.callee"><span class="id" title="projection">Sortclass</span></a>.<br/>
+<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.frame"><span class="id" title="projection">frame</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.frame"><span class="id" title="projection">:</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.frame"><span class="id" title="projection">type</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.frame"><span class="id" title="projection">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.frame"><span class="id" title="projection">call_of</span></a>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="NonPropType.Exports.notProp"><span class="id" title="abbreviation">notProp</span></a> <span class="id" title="var">T</span> := (@<a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.check"><span class="id" title="definition">check</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.test_negative"><span class="id" title="definition">test_negative</span></a> (<a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.call"><span class="id" title="definition">call</span></a> <span class="id" title="var">T</span>)).<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType.Exports"><span class="id" title="module">Exports</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#NonPropType"><span class="id" title="module">NonPropType</span></a>.<br/>
+<span class="id" title="keyword">Export</span> <span class="id" title="var">NonPropType.Exports</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Module</span> <a name="Deprecation"><span class="id" title="module">Deprecation</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="Deprecation.hidden"><span class="id" title="definition">hidden</span></a> (<span class="id" title="var">T</span> : <span class="id" title="keyword">Type</span>) := <a class="idref" href="mathcomp.ssreflect.ssreflect.html#T"><span class="id" title="variable">T</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="Deprecation.exposed"><span class="id" title="definition">exposed</span></a> (<span class="id" title="var">T</span> : <span class="id" title="keyword">Type</span>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> := <a class="idref" href="mathcomp.ssreflect.ssreflect.html#T"><span class="id" title="variable">T</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="Deprecation.hide"><span class="id" title="definition">hide</span></a> <span class="id" title="var">T</span> <span class="id" title="var">u</span> (<span class="id" title="var">v</span> : <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.exposed"><span class="id" title="definition">exposed</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#u"><span class="id" title="variable">u</span></a>) : <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.hidden"><span class="id" title="definition">hidden</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#T"><span class="id" title="variable">T</span></a> := <a class="idref" href="mathcomp.ssreflect.ssreflect.html#v"><span class="id" title="variable">v</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Ltac</span> <span class="id" title="var">warn</span> <span class="id" title="var">old_id</span> <span class="id" title="var">new_id</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="tactic">idtac</span> "Warning:" <span class="id" title="var">old_id</span> "is deprecated; use" <span class="id" title="var">new_id</span> "instead".<br/>
+
+<br/>
+<span class="id" title="keyword">Ltac</span> <span class="id" title="var">stop</span> <span class="id" title="var">old_id</span> <span class="id" title="var">new_id</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="tactic">fail</span> 1 "Error:" <span class="id" title="var">old_id</span> "is deprecated; use" <span class="id" title="var">new_id</span> "instead".<br/>
+
+<br/>
+<span class="id" title="keyword">Structure</span> <a name="Deprecation.hinted"><span class="id" title="record">hinted</span></a> := <a name="Deprecation.Hint"><span class="id" title="constructor">Hint</span></a> {<a name="Deprecation.statement"><span class="id" title="projection">statement</span></a>; <a name="Deprecation.hint"><span class="id" title="projection">hint</span></a> : <a class="idref" href="mathcomp.ssreflect.ssreflect.html#statement"><span class="id" title="method">statement</span></a>}.<br/>
+<span class="id" title="keyword">Ltac</span> <span class="id" title="var">check</span> <span class="id" title="var">cond</span> := <span class="id" title="keyword">let</span> <span class="id" title="var">test</span> := <span class="id" title="keyword">constr</span>:(<a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.hint"><span class="id" title="projection">hint</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <span class="id" title="var">cond</span>) <span class="id" title="tactic">in</span> <span class="id" title="tactic">idtac</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variant</span> <a name="Deprecation.reject"><span class="id" title="inductive">reject</span></a> := <a name="Deprecation.Reject"><span class="id" title="constructor">Reject</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="Deprecation.reject_hint"><span class="id" title="definition">reject_hint</span></a> := <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.Hint"><span class="id" title="constructor">Hint</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.reject"><span class="id" title="inductive">reject</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.Reject"><span class="id" title="constructor">Reject</span></a>.<br/>
+<span class="id" title="keyword">Module</span> <a name="Deprecation.Reject"><span class="id" title="module">Reject</span></a>. <span class="id" title="var">Canonical</span> <span class="id" title="var">reject_hint</span>. <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.Reject"><span class="id" title="module">Reject</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variant</span> <a name="Deprecation.silent"><span class="id" title="inductive">silent</span></a> := <a name="Deprecation.Silent"><span class="id" title="constructor">Silent</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="Deprecation.silent_hint"><span class="id" title="definition">silent_hint</span></a> := <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.Hint"><span class="id" title="constructor">Hint</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.silent"><span class="id" title="inductive">silent</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.Silent"><span class="id" title="constructor">Silent</span></a>.<br/>
+<span class="id" title="keyword">Module</span> <a name="Deprecation.Silent"><span class="id" title="module">Silent</span></a>. <span class="id" title="var">Canonical</span> <span class="id" title="var">silent_hint</span>. <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.Silent"><span class="id" title="module">Silent</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Ltac</span> <span class="id" title="var">flag</span> <span class="id" title="var">old_id</span> <span class="id" title="var">new_id</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="tactic">first</span> [<span class="id" title="var">check</span> <span class="id" title="var">reject</span>; <span class="id" title="var">stop</span> <span class="id" title="var">old_id</span> <span class="id" title="var">new_id</span> | <span class="id" title="var">check</span> <span class="id" title="var">silent</span> | <span class="id" title="var">warn</span> <span class="id" title="var">old_id</span> <span class="id" title="var">new_id</span>].<br/>
+
+<br/>
+<span class="id" title="keyword">Module</span> <a name="Deprecation.Exports"><span class="id" title="module">Exports</span></a>.<br/>
+<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.hide"><span class="id" title="definition">hide</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.hide"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.hide"><span class="id" title="definition">exposed</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.hide"><span class="id" title="definition">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.hide"><span class="id" title="definition">hidden</span></a>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="Deprecation.Exports.deprecate"><span class="id" title="abbreviation">deprecate</span></a> <span class="id" title="var">old_id</span> <span class="id" title="var">new_id</span> :=<br/>
+&nbsp;&nbsp;(<a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.hide"><span class="id" title="definition">hide</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">old_id</span> <span class="id" title="var">new_id</span> ⇒ <span class="id" title="keyword">ltac</span>:(<span class="id" title="var">flag</span> <span class="id" title="var">old_id</span> <span class="id" title="var">new_id</span>; <span class="id" title="tactic">exact</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#tt"><span class="id" title="constructor">tt</span></a>)) <span class="id" title="var">new_id</span>)<br/>
+&nbsp;&nbsp;(<span class="id" title="var">only</span> <span class="id" title="var">parsing</span>).<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.Exports"><span class="id" title="module">Exports</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation"><span class="id" title="module">Deprecation</span></a>.<br/>
+<span class="id" title="keyword">Export</span> <span class="id" title="var">Deprecation.Exports</span>.<br/>
+</div>
 </div>
 
 <div id="footer">