Refactor bibliography

doc/chapter-powers.tex

@@ -333,7 +333,7 @@ \subsection{Computing Fibonacci numbers}
 present ways to compute Fibonacci numbers, with the less number of recursive calls  as possible. Please note that these optimizations and the formal proof of their correctness are \emph{ad-hoc}, \emph{i.e.} exclusively written for the 
 Fibonacci numbers.
 In contrast, the optimizations we present in this document apply, in their vast majority, \emph{generic} techniques of efficient computation of powers in a monoid. 
-This example of Fibonacci numbers has been developed with Yves Bertot, who wrote a first version with \texttt{SSreflect/Mathcomp}~\cite{MCB, SSR}. 
+This example of Fibonacci numbers has been developed with Yves Bertot, who wrote a first version with \texttt{SSreflect/Mathcomp}~\cite{MCB}.
 
 
 \subsubsection{Using 2x2 integer matrices}
@@ -1287,7 +1287,7 @@ \subsection{Refinement and correctness}
 The relationship between \texttt{power} and \texttt{N\_bpow} can be considered
 as a kind of \emph{refinement} as in the \texttt{B}-method~\cite{b-book}. Note
 that the two representations of natural numbers and the function \texttt{N.to\_nat}
-form a kind of  \emph{data refinement} \cite{Abrial:2010:MES:1855020, cohen:hal-01113453}.
+form a kind of  \emph{data refinement} \cite{Abrial:2010:MES:1855020, Cohen2013}.
 
 
 

doc/part-hydras.tex

@@ -2557,7 +2557,7 @@ \section{A notation for finite ordinals}
 \end{remark}
 
 \begin{remark}
-Finite ordinals are also formalized in MathComp~\cite{SSR}.  See also Adam Chlipala's \emph{CPDT}~\cite{chlipalacpdt2011} for a thorough study of the use of dependent types.  
+Finite ordinals are also formalized in MathComp~\cite{MCB}.  See also Adam Chlipala's \emph{CPDT}~\cite{chlipalacpdt2011} for a thorough study of the use of dependent types.  
 \end{remark}