From 5eae5b130f87aabdfee23bbc9f4114fb5c0624b1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 14 Apr 2008 22:34:19 +0000
Subject: Diverses corrections

- gestion des idents (suite commit 10785) [lib, interp, contrib/ring, dev]
- suppression (enfin) des $id dans les constr (utilisation des MetaIdArg des
  quotations de tactiques pour simuler les métas des constr - quitte à devoir
  utiliser un let-in dans l'expression de tactique) [proofs, parsing, tactics]
- utilisation de error en place d'un "print_string" d'échec dans fourier
- améliorations espérées vis à vis de quelques "bizarreries" dans la gestion
  des Meta [pretyping]



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10790 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/util.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'lib')

diff --git a/lib/util.ml b/lib/util.ml
index b317c849cc..ccd807a90a 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -290,6 +290,7 @@ let check_ident s =
     | _ -> error (s^": an identifier should start with a letter")
   with 
   | End_of_input -> error "The empty string is not an identifier"
+  | UnsupportedUtf8 -> error (s^": unsupported character in utf8 sequence")
   | Invalid_argument _ -> error (s^": invalid utf8 sequence")
 
 (* Lists *)
-- 
cgit v1.2.3