aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_xml.ml4
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-12-24 23:49:21 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-12-24 23:49:21 +0000
commitd33ced344ba377f0a4003102d77f880fda108fd7 (patch)
treea8f7642bb599a08ada8b6392d0fa14f823e57e3c /parsing/g_xml.ml4
parent6ebd4c4ad28d46965623e72d8654c36fcc6fe9b0 (diff)
More {raw => glob} changes for consistency
perl -pi -e 's/(\W|_)raw((?:sort|_prop|terms?|_branch|_red_flag|pat tern|_constr_of|_of_pat)(?:\W|_))/\1glob_\2/g;s/glob__/glob_/g;s/(\ W)R((?:Prop|Type|Fix|CoFix|StructRec|WfRec|MeasureRec)\W)/\1G\2/g;s /glob_terms?/glob_constr/g' **/*.ml* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13756 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_xml.ml4')
-rw-r--r--parsing/g_xml.ml418
1 files changed, 9 insertions, 9 deletions
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 18bc1ff78..72634b08e 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -95,9 +95,9 @@ let inductive_of_cdata a = match global_of_cdata a with
let ltacref_of_cdata (loc,a) = (loc,locate_tactic (uri_of_data a))
let sort_of_cdata (loc,a) = match a with
- | "Prop" -> RProp Null
- | "Set" -> RProp Pos
- | "Type" -> RType None
+ | "Prop" -> GProp Null
+ | "Set" -> GProp Pos
+ | "Type" -> GType None
| _ -> user_err_loc (loc,"",str "sort expected.")
let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al)
@@ -184,10 +184,10 @@ let rec interp_xml_constr = function
let li,lnct = List.split (List.map interp_xml_FixFunction xl) in
let ln,lc,lt = list_split3 lnct in
let lctx = List.map (fun _ -> []) ln in
- GRec (loc, RFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, Array.of_list lctx, Array.of_list lc, Array.of_list lt)
+ GRec (loc, GFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, Array.of_list lctx, Array.of_list lc, Array.of_list lt)
| XmlTag (loc,"COFIX",al,xl) ->
let ln,lc,lt = list_split3 (List.map interp_xml_CoFixFunction xl) in
- GRec (loc, RCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt)
+ GRec (loc, GCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt)
| XmlTag (loc,"CAST",al,[x1;x2]) ->
GCast (loc, interp_xml_term x1, CastConv (DEFAULTcast, interp_xml_type x2))
| XmlTag (loc,"SORT",al,[]) ->
@@ -229,15 +229,15 @@ and interp_xml_recursionOrder x =
let (locs, s) = get_xml_attr "type" al in
match s with
"Structural" ->
- (match l with [] -> RStructRec
+ (match l with [] -> GStructRec
| _ -> error_expect_no_argument loc)
| "WellFounded" ->
(match l with
- [c] -> RWfRec (interp_xml_type c)
+ [c] -> GWfRec (interp_xml_type c)
| _ -> error_expect_one_argument loc)
| "Measure" ->
(match l with
- [m;r] -> RMeasureRec (interp_xml_type m, Some (interp_xml_type r))
+ [m;r] -> GMeasureRec (interp_xml_type m, Some (interp_xml_type r))
| _ -> error_expect_two_arguments loc)
| _ ->
user_err_loc (locs,"",str "Invalid recursion order.")
@@ -249,7 +249,7 @@ and interp_xml_FixFunction x =
interp_xml_recursionOrder x1),
(get_xml_name al, interp_xml_type x2, interp_xml_body x3))
| (loc,al,[x1;x2]) ->
- ((Some (nmtoken (get_xml_attr "recIndex" al)), RStructRec),
+ ((Some (nmtoken (get_xml_attr "recIndex" al)), GStructRec),
(get_xml_name al, interp_xml_type x1, interp_xml_body x2))
| (loc,_,_) ->
error_expect_one_argument loc