aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/syntax/ascii_syntax.ml
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-12-23 18:50:45 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-12-23 18:50:45 +0000
commit8f9461509338a3ebba46faaad3116c4e44135423 (patch)
tree23da64d38f2194a1f9e42b789b16b82402d6908f /plugins/syntax/ascii_syntax.ml
parentfafba6b545c7d0d774bcd79bdbddb8869517aabb (diff)
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
Diffstat (limited to 'plugins/syntax/ascii_syntax.ml')
-rw-r--r--plugins/syntax/ascii_syntax.ml12
1 files changed, 6 insertions, 6 deletions
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 79e1a6eb2..50498f0f4 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -39,9 +39,9 @@ let interp_ascii dloc p =
let rec aux n p =
if n = 0 then [] else
let mp = p mod 2 in
- RRef (dloc,if mp = 0 then glob_false else glob_true)
+ GRef (dloc,if mp = 0 then glob_false else glob_true)
:: (aux (n-1) (p/2)) in
- RApp (dloc,RRef(dloc,force glob_Ascii), aux 8 p)
+ GApp (dloc,GRef(dloc,force glob_Ascii), aux 8 p)
let interp_ascii_string dloc s =
let p =
@@ -57,12 +57,12 @@ let interp_ascii_string dloc s =
let uninterp_ascii r =
let rec uninterp_bool_list n = function
| [] when n = 0 -> 0
- | RRef (_,k)::l when k = glob_true -> 1+2*(uninterp_bool_list (n-1) l)
- | RRef (_,k)::l when k = glob_false -> 2*(uninterp_bool_list (n-1) l)
+ | GRef (_,k)::l when k = glob_true -> 1+2*(uninterp_bool_list (n-1) l)
+ | GRef (_,k)::l when k = glob_false -> 2*(uninterp_bool_list (n-1) l)
| _ -> raise Non_closed_ascii in
try
let rec aux = function
- | RApp (_,RRef (_,k),l) when k = force glob_Ascii -> uninterp_bool_list 8 l
+ | GApp (_,GRef (_,k),l) when k = force glob_Ascii -> uninterp_bool_list 8 l
| _ -> raise Non_closed_ascii in
Some (aux r)
with
@@ -78,4 +78,4 @@ let _ =
Notation.declare_string_interpreter "char_scope"
(ascii_path,ascii_module)
interp_ascii_string
- ([RRef (dummy_loc,static_glob_Ascii)], uninterp_ascii_string, true)
+ ([GRef (dummy_loc,static_glob_Ascii)], uninterp_ascii_string, true)