summaryrefslogtreecommitdiff
path: root/parsing/g_xml.ml4
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /parsing/g_xml.ml4
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'parsing/g_xml.ml4')
-rw-r--r--parsing/g_xml.ml410
1 files changed, 6 insertions, 4 deletions
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index ce284454..5b2d8668 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -6,7 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: g_xml.ml4 10090 2007-08-24 10:53:53Z herbelin $ *)
+(*i camlp4use: "pa_extend.cmo" i*)
+
+(* $Id: g_xml.ml4 10727 2008-03-28 20:22:43Z msozeau $ *)
open Pp
open Util
@@ -139,12 +141,12 @@ let rec interp_xml_constr = function
| XmlTag (loc,"LAMBDA",al,(_::_ as xl)) ->
let body,decls = list_sep_last xl in
let ctx = List.map interp_xml_decl decls in
- List.fold_right (fun (na,t) b -> RLambda (loc, na, t, b))
+ List.fold_right (fun (na,t) b -> RLambda (loc, na, Explicit, t, b))
ctx (interp_xml_target body)
| XmlTag (loc,"PROD",al,(_::_ as xl)) ->
let body,decls = list_sep_last xl in
let ctx = List.map interp_xml_decl decls in
- List.fold_right (fun (na,t) b -> RProd (loc, na, t, b))
+ List.fold_right (fun (na,t) b -> RProd (loc, na, Explicit, t, b))
ctx (interp_xml_target body)
| XmlTag (loc,"LETIN",al,(_::_ as xl)) ->
let body,defs = list_sep_last xl in
@@ -169,7 +171,7 @@ let rec interp_xml_constr = function
let mat = simple_cases_matrix_of_branches ind brns brs in
let nparams,n = compute_inductive_nargs ind in
let nal,rtn = return_type_of_predicate ind nparams n p in
- RCases (loc,rtn,[tm,nal],mat)
+ RCases (loc,RegularStyle,rtn,[tm,nal],mat)
| XmlTag (loc,"MUTIND",al,[]) ->
RRef (loc, IndRef (get_xml_inductive al))
| XmlTag (loc,"MUTCONSTRUCT",al,[]) ->