diff options
| author | herbelin | 2006-07-05 17:19:39 +0000 |
|---|---|---|
| committer | herbelin | 2006-07-05 17:19:39 +0000 |
| commit | ec2a4b3402e901067a4295996028decbd9f6671f (patch) | |
| tree | c0f457f754510453a1dbf0a7ecd7fde065ebd73c | |
| parent | 30f681f2800c1312813781b146baaf8008aae43e (diff) | |
Nettoyage code mort
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9016 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_xml.ml4 | 12 |
1 files changed, 1 insertions, 11 deletions
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 0bd72db4a9..7165f0d103 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -256,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 = |