diff options
| author | msozeau | 2006-03-13 17:38:17 +0000 |
|---|---|---|
| committer | msozeau | 2006-03-13 17:38:17 +0000 |
| commit | db6c97df4dde8b1ccb2e5b314a4747f66fd524c1 (patch) | |
| tree | 39ba546322e7f3d4bd4cc9d58260d3f1b4114bd5 /parsing/g_xml.ml4 | |
| parent | d9cc734c4cd2a75a303cc08c3df0973077099ab1 (diff) | |
Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.
May cause make world to fail because of dependency problems, make depend clean
world should fix that (hopefully).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8624 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_xml.ml4')
| -rw-r--r-- | parsing/g_xml.ml4 | 25 |
1 files changed, 22 insertions, 3 deletions
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 7b7e471c64..1df3d1f256 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -187,12 +187,31 @@ and interp_xml_decl_alias s x = and interp_xml_def x = interp_xml_decl_alias "def" x and interp_xml_decl x = interp_xml_decl_alias "decl" x +and interp_xml_recursionOrder x = + let (loc, al, l) = interp_xml_tag "RecursionOrder" x in + let (locs, s) = get_xml_attr "type" al in + match s with + "Structural" -> + (match l with [] -> RStructRec + | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected none)")) + | "WellFounded" -> + (match l with + [c] -> RWfRec (interp_xml_type c) + | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected one)")) + | _ -> + user_err_loc (locs,"",str "invalid recursion order") + + and interp_xml_FixFunction x = match interp_xml_tag "FixFunction" x with - | (loc,al,[x1;x2]) -> - (nmtoken (get_xml_attr "recIndex" al), + | (loc,al,[x1;x2;x3]) -> + ((nmtoken (get_xml_attr "recIndex" al), + interp_xml_recursionOrder x1), + (get_xml_ident al, interp_xml_type x2, interp_xml_body x3)) + | (loc,al,[x1;x2]) -> (* For backwards compatibility *) + ((nmtoken (get_xml_attr "recIndex" al), RStructRec), (get_xml_ident al, interp_xml_type x1, interp_xml_body x2)) - | (loc,_,_) -> + | (loc,_,_) -> user_err_loc (loc,"",str "wrong number of arguments (expect one)") and interp_xml_CoFixFunction x = |