From faa0de5c67594980f8ad871dcf71c0dc98865a5e Mon Sep 17 00:00:00 2001
From: pboutill
Date: Tue, 18 May 2010 15:57:21 +0000
Subject: Some ocamldoc comments + Fixing name of .coqrc.version file in refman

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13013 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/cases.mli | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 202a794abb..ab1f409ca4 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -15,6 +15,9 @@ open Inductiveops
 open Rawterm
 open Evarutil
 
+(** {5 Compilation of pattern-matching } *)
+
+(** {6 Pattern-matching errors } *)
 type pattern_matching_error =
   | BadPattern of constructor * constr
   | BadConstructor of constructor * inductive
@@ -43,8 +46,8 @@ val error_wrong_predicate_arity_loc : loc -> env -> constr -> constr -> constr -
 val error_needs_inversion : env -> constr -> types -> 'a
 
 val set_impossible_default_clause : constr * types -> unit
-(** {6 Compilation of pattern-matching. } *)
 
+(** {6 Compilation primitive. } *)
 type alias_constr =
   | DepAlias
   | NonDepAlias
-- 
cgit v1.2.3