From 8f9461509338a3ebba46faaad3116c4e44135423 Mon Sep 17 00:00:00 2001 From: glondu Date: Thu, 23 Dec 2010 18:50:45 +0000 Subject: Change of nomenclature: rawconstr -> glob_constr There was a discrepancy of the notions "raw" and "globalized" between constrs and tactics, and some confusion of the notions in e.g. genarg.mli (see all globwit_* there). This commit is a first step towards unification of terminology between constrs and tactics. Changes in module names will be done separately. In extraargs.ml4, the "ARGUMENT EXTEND raw" and related stuff, even affected by this change, has not been touched and highlights another confusion in "ARGUMENT EXTEND" in general that will be addressed later. The funind plugin doesn't respect the same naming conventions as the rest, so leave some "raw" there for now... they will be addressed later. This big commit has been generated with the following command (wrapped here, but should be on a *single* line): perl -pi -e 's/(\W(?:|pp|pr_l)|_)raw((?:constrs?|type|vars|_binder| _context|decl|_decompose|_compose|_make)(?:\W|_))/\1glob_\2/g;s/glo b__/glob_/g;s/prraw/prglob/g;s/(\W)R((?:Ref|Var|Evar|PatVar|App|Lam bda|Prod|LetIn|Cases|LetTuple|If|Rec|Sort|Hole|Cast|Dynamic)\W)/\1G \2/g' `git ls-files|grep -v dev/doc/changes.txt` git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13743 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/syntax/string_syntax.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'plugins/syntax/string_syntax.ml') diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index cb2b16858..61643881e 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -37,8 +37,8 @@ open Lazy let interp_string dloc s = let le = String.length s in let rec aux n = - if n = le then RRef (dloc, force glob_EmptyString) else - RApp (dloc,RRef (dloc, force glob_String), + if n = le then GRef (dloc, force glob_EmptyString) else + GApp (dloc,GRef (dloc, force glob_String), [interp_ascii dloc (int_of_char s.[n]); aux (n+1)]) in aux 0 @@ -46,11 +46,11 @@ let uninterp_string r = try let b = Buffer.create 16 in let rec aux = function - | RApp (_,RRef (_,k),[a;s]) when k = force glob_String -> + | GApp (_,GRef (_,k),[a;s]) when k = force glob_String -> (match uninterp_ascii a with | Some c -> Buffer.add_char b (Char.chr c); aux s | _ -> raise Non_closed_string) - | RRef (_,z) when z = force glob_EmptyString -> + | GRef (_,z) when z = force glob_EmptyString -> Some (Buffer.contents b) | _ -> raise Non_closed_string @@ -62,6 +62,6 @@ let _ = Notation.declare_string_interpreter "string_scope" (string_path,["Coq";"Strings";"String"]) interp_string - ([RRef (dummy_loc,static_glob_String); - RRef (dummy_loc,static_glob_EmptyString)], + ([GRef (dummy_loc,static_glob_String); + GRef (dummy_loc,static_glob_EmptyString)], uninterp_string, true) -- cgit v1.2.3