diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_xml.ml4 | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 72634b08e7..c9e135edcf 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -170,9 +170,10 @@ let rec interp_xml_constr = function let ind = get_xml_inductive al in let p = interp_xml_patternsType x in let tm = interp_xml_inductiveTerm y in - let brs = List.map interp_xml_pattern yl in - let brns = Array.to_list (compute_branches_lengths ind) in - let mat = simple_cases_matrix_of_branches ind brns brs in + let vars = compute_branches_lengths ind in + let brs = list_map_i (fun i c -> (i,vars.(i),interp_xml_pattern c)) 0 yl + in + let mat = simple_cases_matrix_of_branches ind brs in let nparams,n = compute_inductive_nargs ind in let nal,rtn = return_type_of_predicate ind nparams n p in GCases (loc,RegularStyle,rtn,[tm,nal],mat) |