From ddbfb9299340f069a26fc6218e82031a8a99d056 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 7 Feb 2007 19:14:09 +0000
Subject: Meilleur anglais (cf 9619)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9620 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/funind/indfun.ml  | 2 +-
 doc/refman/RefMan-ext.tex | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 82bb286953..6e2af2247b 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -266,7 +266,7 @@ let derive_inversion fix_names =
 	)
     with e -> 
       msg_warning 
-	(str "Cannot built inversion information" ++ 
+	(str "Cannot build functional inversion principle" ++ 
 	   if do_observe () then Cerrors.explain_exn e else mt ())
   with _ -> ()
 
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index e05183ce91..8fdb8d8df7 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -645,7 +645,7 @@ each branch.  For now dependent cases are not treated.
   but the induction principle could not be built. Only the ident is
   defined. Please report.
 
-\item \errindex{Cannot built inversion information} (warning)
+\item \errindex{Cannot build functional inversion principle} (warning)
 
   \texttt{functional inversion} will not be available for the
   function.
-- 
cgit v1.2.3