From eddc388071fc1d1eba06b96732f9b195b88d1054 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 9 Nov 2001 17:26:39 +0000
Subject: MAJ pour make doc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2177 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/inductive.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/inductive.mli')

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index dbaf367889..f4d5b53461 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -59,7 +59,7 @@ val type_case_branches :
   env -> inductive * constr list -> unsafe_judgment -> constr
     -> types array * types * constraints
 
-(* Check a case_info actually correspond to a Case expression on the
+(* Check a [case_info] actually correspond to a Case expression on the
    given inductive type. *)
 val check_case_info : env -> inductive -> case_info -> unit
 
-- 
cgit v1.2.3