diff options
Diffstat (limited to 'parsing/g_xml.ml4')
| -rw-r--r-- | parsing/g_xml.ml4 | 18 |
1 files changed, 6 insertions, 12 deletions
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 5ad0193b..a89fffa0 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_xml.ml4 8875 2006-05-29 19:59:11Z msozeau $ *) +(* $Id: g_xml.ml4 9016 2006-07-05 17:19:39Z herbelin $ *) open Pp open Util @@ -228,6 +228,10 @@ and interp_xml_recursionOrder x = (match l with [c] -> RWfRec (interp_xml_type c) | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected one)")) + | "Measure" -> + (match l with + [c] -> RMeasureRec (interp_xml_type c) + | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected one)")) | _ -> user_err_loc (locs,"",str "invalid recursion order") @@ -252,22 +256,12 @@ and interp_xml_CoFixFunction x = (* Interpreting tactic argument *) -let rec (interp_xml_tactic_expr : xml -> glob_tactic_expr) = function - | XmlTag (loc,"TACARG",[],[x]) -> - TacArg (interp_xml_tactic_arg x) - | _ -> error "Ill-formed xml tree" - -and interp_xml_tactic_arg = function +let rec interp_xml_tactic_arg = function | XmlTag (loc,"TERM",[],[x]) -> ConstrMayEval (ConstrTerm (interp_xml_constr x,None)) | XmlTag (loc,"CALL",al,xl) -> let ltacref = ltacref_of_cdata (get_xml_attr "uri" al) in TacCall(loc,ArgArg ltacref,List.map interp_xml_tactic_arg xl) -(* - | XmlTag (loc,"TACTIC",[],[x]) -> - Tacexp (interp_xml_tactic_expr x) - | _ -> error "Ill-formed xml tree" -*) | XmlTag (loc,s,_,_) -> user_err_loc (loc,"", str "Unexpected tag " ++ str s) let parse_tactic_arg ch = |