From cc00a83aa3153f2d646e0f85aebd521108594f8c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 10 Dec 2002 09:39:58 +0000
Subject: Avertissement plus clair

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

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 4ecd57ba68..7035bfdfa2 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -101,7 +101,10 @@ let idopt_of_name = function
   | Name id -> Some id
   | Anonymous -> None
 
-let extern_evar loc n = warning "No notation for Meta"; CMeta (loc,n)
+let extern_evar loc n =
+  warning
+    "Existential variable turned into meta-variable during externalization";
+  CMeta (loc,n)
 
 let raw_string_of_ref = function
   | ConstRef kn -> 
-- 
cgit v1.2.3