Add patch-framework and patches

Some Coq files are currently not parseable and/or broken. The patches
fix those problems and make the Coq packages accesible.

.patches/cfml

+diff --git a/Coq/CFML/CFHeaps.theory.xml b/Coq/CFML/CFHeaps.theory.xml
+index c972d04..edccc68 100644
+--- a/Coq/CFML/CFHeaps.theory.xml
++++ b/Coq/CFML/CFHeaps.theory.xml
+@@ -484,10 +484,10 @@ Hints  <ht:DEFINITION uri="cic:/CFML/CFHeaps/Hsimpl_hint.ind" as="Inductive" lin
+ Tactics 
+ <br/>
+ Maintain the goal in the form
+-     H1 \* ... \* HN \* <font size=-2>&#9744;</font> ==&gt; HA \* HR
++     H1 \* ... \* HN \* <font size="-2">&#9744;</font> ==&gt; HA \* HR
+    where HA is initially empty and accumulates elements not simplifiable
+    and HR contains the values that are to be cancelled out;
+-   the last item of HR is always a <font size=-2>&#9744;</font>.
++   the last item of HR is always a <font size="-2">&#9744;</font>.
+    As long as HR is of the form H \* H', we try to match H with one of the Hi.
+   <span class="inlinecode"><span class="id" title="var">hsimpls</span></span> is the same as <span class="inlinecode"><span class="id" title="var">hsimpl</span>;</span> <span class="inlinecode"><span class="id" title="tactic">subst</span></span>  <span class="inlinecode"><span class="id" title="var">hsimpl_credits</span></span> is the same as <span class="inlinecode"><span class="id" title="var">hsimpl</span></span> excepts that it tries
+     to perform arithmetic to simplify credits. Note: to execute
+diff --git a/Coq/CFML/CFTactics.theory.xml b/Coq/CFML/CFTactics.theory.xml
+index cc162a2..edda3d4 100644
+--- a/Coq/CFML/CFTactics.theory.xml
++++ b/Coq/CFML/CFTactics.theory.xml
+@@ -1699,7 +1699,7 @@ Tactic Notation "xlets" constr(Q) :=
+ 
+ <br/>
+ Tactic <span class="inlinecode"><span class="id" title="var">xskip_credits</span></span> eliminates all occurrences of credits
+-    in the goal, by replacing <span class="inlinecode">\$</span> <span class="inlinecode"><span class="id" title="var">x</span></span> with the empty heap predicate \<font size=-2>&#9744;</font>.
++    in the goal, by replacing <span class="inlinecode">\$</span> <span class="inlinecode"><span class="id" title="var">x</span></span> with the empty heap predicate \<font size="-2">&#9744;</font>.
+ 
+ <div class="paragraph"> </div>
+ 

.patches/coquelicot

+diff --git a/Coq/Coquelicot/PSeries.theory.xml b/Coq/Coquelicot/PSeries.theory.xml
+index dea0fcb..31b023a 100644
+--- a/Coq/Coquelicot/PSeries.theory.xml
++++ b/Coq/Coquelicot/PSeries.theory.xml
+@@ -60,7 +60,7 @@ COPYING file for more details.
+  <ht:REQUIRE uri="cic:/Coquelicot/Derive"/>
+  <ht:REQUIRE uri="cic:/Coquelicot/Seq_fct"/>
+  <ht:REQUIRE uri="cic:/Coquelicot/Series"/>
+- This file describes power series: &Sigma; a<sub>k</sub>
++ This file describes power series: Sigma a<sub>k</sub>
+ x<sup>k</sup>. It contains definition, equivalence with the standard
+ library, differentiability, integrability, and many results about the
+ convergence circle.  <ht:SECTION uri="cic:/Coquelicot/PSeries/Definitions" line="32">
+diff --git a/Coq/Coquelicot/Rbar.theory.xml b/Coq/Coquelicot/Rbar.theory.xml
+index c27518c..97cab72 100644
+--- a/Coq/Coquelicot/Rbar.theory.xml
++++ b/Coq/Coquelicot/Rbar.theory.xml
+@@ -49,7 +49,7 @@ COPYING file for more details.
+  <ht:REQUIRE uri="cic:/mathcomp/ssreflect/ssreflect"/>
+  <ht:REQUIRE uri="cic:/Coquelicot/Rcomplements"/>
+  This file contains the definition and properties of the set
+- <span class="inlinecode"><span class="id" title="var">R</span></span>  &#8746; {+ &infin;} &#8746; {- &infin;}  denoted by <span class="inlinecode"><span class="id" title="var">Rbar</span></span>. We have defined:
++ <span class="inlinecode"><span class="id" title="var">R</span></span>  &#8746; {+ infin} &#8746; {- infin}  denoted by <span class="inlinecode"><span class="id" title="var">Rbar</span></span>. We have defined:
+ <ul class="doclist">
+ <li> coercions from <span class="inlinecode"><span class="id" title="var">R</span></span> to <span class="inlinecode"><span class="id" title="var">Rbar</span></span> and vice versa (<span class="inlinecode"><span class="id" title="var">Finite</span></span> gives <span class="inlinecode"><span class="id" title="var">R0</span></span> at infinity points)
+ 

.patches/flocq

+diff --git a/Coq/Flocq/Core/Raux.theory.xml b/Coq/Flocq/Core/Raux.theory.xml
+index d0464f6..5949443 100644
+--- a/Coq/Flocq/Core/Raux.theory.xml
++++ b/Coq/Flocq/Core/Raux.theory.xml
+@@ -290,7 +290,7 @@ COPYING file for more details.
+ 
+  <ht:THEOREM uri="cic:/Flocq/Core/Raux/radix_pos.con" as="Theorem" line="1333"/>
+ 
+- Well-used function called bpow for computing the power function &beta;^e  <ht:DEFINITION uri="cic:/Flocq/Core/Raux/bpow.con" as="Definition" line="1336"/>
++ Well-used function called bpow for computing the power function beta^e  <ht:DEFINITION uri="cic:/Flocq/Core/Raux/bpow.con" as="Definition" line="1336"/>
+ 
+  <ht:THEOREM uri="cic:/Flocq/Core/Raux/IZR_Zpower_pos.con" as="Theorem" line="1357"/>
+ 
+@@ -328,7 +328,7 @@ COPYING file for more details.
+ 
+  <ht:THEOREM uri="cic:/Flocq/Core/Raux/sqrt_bpow_ge.con" as="Lemma" line="1571"/>
+ 
+- Another well-used function for having the magnitude of a real number x to the base &beta;  <ht:DEFINITION uri="cic:/Flocq/Core/Raux/mag_prop.ind" as="Inductive" line="1574"/>
++ Another well-used function for having the magnitude of a real number x to the base beta  <ht:DEFINITION uri="cic:/Flocq/Core/Raux/mag_prop.ind" as="Inductive" line="1574"/>
+ 
+  <ht:DEFINITION uri="cic:/Flocq/Core/Raux/mag_val.con" as="Projection" line="1574"/>
+ 
+diff --git a/Coq/Flocq/Pff/Pff.theory.xml b/Coq/Flocq/Pff/Pff.theory.xml
+index 19bdd6b..16bcab8 100644
+--- a/Coq/Flocq/Pff/Pff.theory.xml
++++ b/Coq/Flocq/Pff/Pff.theory.xml
+@@ -3148,22 +3148,22 @@ It is the work of Sylvie Boldo, Marc Daumas, Laurence Rideau, and Laurent Théry
+  </ht:SECTION>
+ <a name="lab32"></a><h1 class="section">was file discriminant2.v</h1>
+  This proof file has been written by
+-<A href="http://perso.ens-lyon.fr/sylvie.boldo/">Sylvie Boldo</A>(1), following a proof
+-presented by <A HREF="http://www.cs.berkeley.edu/~wkahan/">Pr William Kahan</A> (2),
++<a href="http://perso.ens-lyon.fr/sylvie.boldo/">Sylvie Boldo</a>(1), following a proof
++presented by <a HREF="http://www.cs.berkeley.edu/~wkahan/">Pr William Kahan</a> (2),
+ and adapted to Coq proof checker with the help of
+-<A href="http://perso.ens-lyon.fr/guillaume.melquiond/">Guillaume Melquiond</A>(1)
+-and <A href="http://perso.ens-lyon.fr/marc.daumas/">Marc Daumas</A>(1). This work
+-has been partially supported by the <A HREF="http://www.cnrs.fr">CNRS</A> grant PICS 2533.
++<a href="http://perso.ens-lyon.fr/guillaume.melquiond/">Guillaume Melquiond</a>(1)
++and <a href="http://perso.ens-lyon.fr/marc.daumas/">Marc Daumas</a>(1). This work
++has been partially supported by the <a HREF="http://www.cnrs.fr">CNRS</a> grant PICS 2533.
+ 
+ <div class="paragraph"> </div>
+ 
+-(1) <A HREF="http://www.ens-lyon.fr/LIP/">LIP</A> Computer science laboratory
++(1) <a HREF="http://www.ens-lyon.fr/LIP/">LIP</a> Computer science laboratory
+ UMR 5668 CNRS - ENS de Lyon - INRIA
+ Lyon, France
+ 
+ <div class="paragraph"> </div>
+ 
+-(2) <a href="http://www.berkeley.edu/">University of California at Berkeley</A>
++(2) <a href="http://www.berkeley.edu/">University of California at Berkeley</a>
+ Berkeley, California
+  <ht:SECTION uri="cic:/Flocq/Pff/Pff/Discriminant1" line="19370">
+  <ht:VARIABLE uri="cic:/Flocq/Pff/Pff/Discriminant1/bo.var" as="Assumption" line="19371"/>
+@@ -4308,22 +4308,22 @@ Berkeley, California
+  </ht:SECTION>
+ <a name="lab34"></a><h1 class="section">was file discriminant.v</h1>
+  This proof file has been written by
+-<A href="http://perso.ens-lyon.fr/sylvie.boldo/">Sylvie Boldo</A>(1), following a proof
+-presented by <A HREF="http://www.cs.berkeley.edu/~wkahan/">Pr William Kahan</A> (2),
++<a href="http://perso.ens-lyon.fr/sylvie.boldo/">Sylvie Boldo</a>(1), following a proof
++presented by <a HREF="http://www.cs.berkeley.edu/~wkahan/">Pr William Kahan</a> (2),
+ and adapted to Coq proof checker with the help of
+-<A href="http://perso.ens-lyon.fr/guillaume.melquiond/">Guillaume Melquiond</A>(1)
+-and <A href="http://perso.ens-lyon.fr/marc.daumas/">Marc Daumas</A>(1). This work
+-has been partially supported by the <A HREF="http://www.cnrs.fr">CNRS</A> grant PICS 2533.
++<a href="http://perso.ens-lyon.fr/guillaume.melquiond/">Guillaume Melquiond</a>(1)
++and <a href="http://perso.ens-lyon.fr/marc.daumas/">Marc Daumas</a>(1). This work
++has been partially supported by the <a HREF="http://www.cnrs.fr">CNRS</a> grant PICS 2533.
+ 
+ <div class="paragraph"> </div>
+ 
+-(1) <A HREF="http://www.ens-lyon.fr/LIP/">LIP</A> Computer science laboratory
++(1) <a HREF="http://www.ens-lyon.fr/LIP/">LIP</a> Computer science laboratory
+ UMR 5668 CNRS - ENS de Lyon - INRIA
+ Lyon, France
+ 
+ <div class="paragraph"> </div>
+ 
+-(2) <a href="http://www.berkeley.edu/">University of California at Berkeley</A>
++(2) <a href="http://www.berkeley.edu/">University of California at Berkeley</a>
+ Berkeley, California
+  <ht:SECTION uri="cic:/Flocq/Pff/Pff/Discriminant5B" line="23211">
+  <ht:VARIABLE uri="cic:/Flocq/Pff/Pff/Discriminant5B/bo.var" as="Assumption" line="23212"/>
+diff --git a/Coq/Flocq/Prop/Relative.theory.xml b/Coq/Flocq/Prop/Relative.theory.xml
+index 521b72b..94bf766 100644
+--- a/Coq/Flocq/Prop/Relative.theory.xml
++++ b/Coq/Flocq/Prop/Relative.theory.xml
+@@ -83,7 +83,7 @@ COPYING file for more details.
+ 
+  <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error.con" as="Theorem" line="154"/>
+ 
+- 1+&epsilon; property in any rounding  <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_ex.con" as="Theorem" line="168"/>
++ 1+epsilon property in any rounding  <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_ex.con" as="Theorem" line="168"/>
+ 
+  <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_F2R_emin.con" as="Theorem" line="183"/>
+ 
+@@ -97,7 +97,7 @@ COPYING file for more details.
+ 
+  <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_N.con" as="Theorem" line="290"/>
+ 
+- 1+&epsilon; property in rounding to nearest  <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_N_ex.con" as="Theorem" line="307"/>
++ 1+epsilon property in rounding to nearest  <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_N_ex.con" as="Theorem" line="307"/>
+ 
+ <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_N_F2R_emin.con" as="Theorem" line="329"/>
+ 
+@@ -121,7 +121,7 @@ COPYING file for more details.
+ 
+  <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_FLX.con" as="Theorem" line="446"/>
+ 
+- 1+&epsilon; property in any rounding in FLX  <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_FLX_ex.con" as="Theorem" line="458"/>
++ 1+epsilon property in any rounding in FLX  <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_FLX_ex.con" as="Theorem" line="458"/>
+ 
+  <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_FLX_round.con" as="Theorem" line="472"/>
+ 
+@@ -141,7 +141,7 @@ COPYING file for more details.
+ 
+  <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_N_FLX'.con" as="Theorem" line="573"/>
+ 
+- 1+&epsilon; property in rounding to nearest in FLX  <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_N_FLX_ex.con" as="Theorem" line="589"/>
++ 1+epsilon property in rounding to nearest in FLX  <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_N_FLX_ex.con" as="Theorem" line="589"/>
+ 
+  <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_N_FLX'_ex.con" as="Theorem" line="601"/>
+ 
+@@ -171,13 +171,13 @@ COPYING file for more details.
+ 
+  <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_FLT_F2R_emin_ex.con" as="Theorem" line="710"/>
+ 
+- 1+&epsilon; property in any rounding in FLT  <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_FLT_ex.con" as="Theorem" line="723"/>
++ 1+epsilon property in any rounding in FLT  <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_FLT_ex.con" as="Theorem" line="723"/>
+ 
+  <ht:VARIABLE uri="cic:/Flocq/Prop/Relative/Fprop_relative/Fprop_relative_FLT/choice.var" as="Assumption" line="725"/>
+ 
+  <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_N_FLT.con" as="Theorem" line="735"/>
+ 
+- 1+&epsilon; property in rounding to nearest in FLT  <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_N_FLT_ex.con" as="Theorem" line="752"/>
++ 1+epsilon property in rounding to nearest in FLT  <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_N_FLT_ex.con" as="Theorem" line="752"/>
+ 
+  <ht:THEOREM uri="cic:/Flocq/Prop/Relative/relative_error_N_FLT_round.con" as="Theorem" line="762"/>
+ 

.patches/mathcomp-algebra

+diff --git a/Coq/mathcomp/algebra/ssralg.theory.xml b/Coq/mathcomp/algebra/ssralg.theory.xml
+index 459d3a22..b93650a2 100644
+--- a/Coq/mathcomp/algebra/ssralg.theory.xml
++++ b/Coq/mathcomp/algebra/ssralg.theory.xml
+@@ -4069,3 +4069,5 @@
+ 
+  <ht:DEFINITION uri="cic:/mathcomp/algebra/ssralg/pair_unitAlgType.con" as="CanonicalStructure" line="6223"/>
+ 
++ </body>
++</html>
+diff --git a/Coq/mathcomp/algebra/vector.theory.xml b/Coq/mathcomp/algebra/vector.theory.xml
+index 81a43dd6..2f70a12c 100644
+--- a/Coq/mathcomp/algebra/vector.theory.xml
++++ b/Coq/mathcomp/algebra/vector.theory.xml
+@@ -230,3 +230,6 @@
+ 
+  <ht:VARIABLE uri="cic:/mathcomp/algebra/vector/VectorTheory/vT.var" as="Assumption" line="367"/>
+ 
++ </ht:SECTION>
++ </body>
++</html>

apply_patches.sh

+#!/bin/bash
+
+PATCHDIR=".patches"
+
+apply_patches() {
+	for patch in "$PATCHDIR"/*; do
+		git -C "$(basename "$patch")" apply "../$patch"
+	done
+}
+
+create_patches() {
+	rm -f "$PATCHDIR"/*
+	git submodule foreach -q "git diff > ../$PATCHDIR/"'$name'
+	find "$PATCHDIR" -type f -empty -delete
+}
+
+if [ "$1" == "-c" ]; then
+	create_patches
+else
+	apply_patches
+fi