diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-13 22:38:00 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-13 22:38:00 +0000 |
| commit | 1d436a18f2f72b57ea09a6d27709a36b63be863a (patch) | |
| tree | 0082ab298988502105c7f71baa5a240051b82fdf /interp | |
| 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')
| -rw-r--r-- | interp/constrextern.ml | 2 | ||||
| -rw-r--r-- | interp/constrintern.ml | 2 | ||||
| -rw-r--r-- | interp/notation.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index b651053db..6cfe74382 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -282,7 +282,7 @@ let drop_implicits_in_patt cst nb_expl args = let has_curly_brackets ntn = String.length ntn >= 6 & (String.sub ntn 0 6 = "{ _ } " or String.sub ntn (String.length ntn - 6) 6 = " { _ }" or - string_string_contains ~where:ntn ~what:" { _ } ") + String.string_contains ~where:ntn ~what:" { _ } ") let rec wildcards ntn n = if n = String.length ntn then [] diff --git a/interp/constrintern.ml b/interp/constrintern.ml index a6b207c1d..cb95af733 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -137,7 +137,7 @@ let explain_non_linear_pattern id = str "The variable " ++ pr_id id ++ str " is bound several times in pattern" let explain_bad_patterns_number n1 n2 = - str "Expecting " ++ int n1 ++ str (plural n1 " pattern") ++ + str "Expecting " ++ int n1 ++ str (String.plural n1 " pattern") ++ str " but found " ++ int n2 let explain_internalization_error e = diff --git a/interp/notation.ml b/interp/notation.ml index d7f539f2f..8483e18a9 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 |