diff options
| author | ppedrot | 2012-11-13 22:38:00 +0000 |
|---|---|---|
| committer | ppedrot | 2012-11-13 22:38:00 +0000 |
| commit | 1d436a18f2f72b57ea09a6d27709a36b63be863a (patch) | |
| tree | 0082ab298988502105c7f71baa5a240051b82fdf /interp/notation.ml | |
| parent | 81ca535c9888bc578d8f9274568ace0d8e7b2d35 (diff) | |
Added a CString module.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15968 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index d7f539f2f7..8483e18a99 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -641,7 +641,7 @@ let decompose_notation_key s = let tok = match String.sub s n (pos-n) with | "_" -> NonTerminal (id_of_string "_") - | s -> Terminal (drop_simple_quotes s) in + | s -> Terminal (String.drop_simple_quotes s) in decomp_ntn (tok::dirs) (pos+1) in decomp_ntn [] 0 |