From 9cf6b3543bf369ccb4d3b0909ee3db96e074e24e Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 10 Feb 2010 00:14:07 +0000
Subject: Fix [Existing Class] impl and add documentation. Fix computation of
 the dependency order of obligations that was not backwards-compatible.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12719 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/Classes.tex | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'doc')

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 1ea07f79a2..7bd4f3522d 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -305,6 +305,10 @@ parameters {\binder$_1$} to {\binder$_n$} and fields {\tt field$_1$} to
   proof size by not inserting useless projections. The class
   constant itself is declared rigid during resolution so that the class 
   abstraction is maintained.  
+
+\item \label{ExistingClass} {\tt Existing Class {\ident}.\comindex{Existing Class}}
+  This variant declares a class a posteriori from a constant or
+  inductive definition. No methods or instances are defined.
 \end{Variants}
 
 \subsection{\tt Instance {\ident} {\binder$_1$ \ldots \binder$_n$} :
-- 
cgit v1.2.3