# Changeset 2416 for Papers/polymorphic-variants-2012

Ignore:
Timestamp:
Oct 25, 2012, 12:30:01 PM (8 years ago)
Message:

Some more minor changes

Location:
Papers/polymorphic-variants-2012
Files:
2 edited

### Legend:

Unmodified
 r2414 \begin{minipage}[b]{0.45\linewidth} \begin{lstlisting} \end{lstlisting} \end{minipage} \subsection{Matita} \label{subsect.matita} Matita~\cite{asperti:user:2007} is a dependently-typed proof assistant developed in Bologna, implementing the Calculus of (Co)inductive Constructions, a type theory similar to that of Coq. Throughout this paper, all running examples are provided in Matita's proof script vernacular. This vernacular, similar to the syntax of OCaml or Coq, should be mostly straightforward. One possible source of confusion is our use of $?$ and $\ldots$, which correspond to a term, or terms, to be inferred automatically by unification, respectively. Any terms that cannot be inferred by unification from the surrounding context are left for the user to provide as proof obligations. Matita \subsection{Subtyping as instantiation vs subtyping as safe static cast}