diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-13 22:38:16 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-13 22:38:16 +0000 |
| commit | 98f3621b5b0c50aaa48c86e1d6a4269d94388bd3 (patch) | |
| tree | e7ecad4d80598956e9aeda2f5c82302ab7e0bde8 /lib/util.ml | |
| parent | 1d436a18f2f72b57ea09a6d27709a36b63be863a (diff) | |
More monomorphizations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15969 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/util.ml')
| -rw-r--r-- | lib/util.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/util.ml b/lib/util.ml index fcbd969ab..8d8c947c7 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -29,7 +29,7 @@ let pi3 (_,_,a) = a let is_letter c = (c >= 'a' && c <= 'z') or (c >= 'A' && c <= 'Z') let is_digit c = (c >= '0' && c <= '9') let is_ident_tail c = - is_letter c or is_digit c or c = '\'' or c = '_' + is_letter c or is_digit c || c = '\'' or c = '_' let is_blank = function | ' ' | '\r' | '\t' | '\n' -> true | _ -> false |