diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-06-22 12:51:04 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-06-22 12:51:04 +0000 |
| commit | 098236cf193fb98d2990c6d52d53a4d4b3f72ba0 (patch) | |
| tree | 8e96f7176a21d4b338ecf38c66bbf4a9465b5294 /parsing | |
| parent | 0f03185388e6d4d2ac376e2e8120437a6ae471b7 (diff) | |
Added {measure x f} as a valid recursion order.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8969 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 1 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 1 | ||||
| -rw-r--r-- | parsing/g_xml.ml4 | 4 | ||||
| -rw-r--r-- | parsing/ppconstr.ml | 2 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 3 |
5 files changed, 11 insertions, 0 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 82e111425..2a975a964 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -244,6 +244,7 @@ GEXTEND Gram fixannot: [ [ "{"; IDENT "struct"; id=name; "}" -> (Some id, CStructRec) | "{"; IDENT "wf"; id=name; rel=lconstr; "}" -> (Some id, CWfRec rel) + | "{"; IDENT "measure"; id=name; rel=lconstr; "}" -> (Some id, CMeasureRec rel) | -> (None, CStructRec) ] ] ; diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 404e7e0df..68ef98749 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -237,6 +237,7 @@ GEXTEND Gram rec_annotation: [ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec) | "{"; IDENT "wf"; id=IDENT; rel=lconstr; "}" -> (Some (id_of_string id), CWfRec rel) + | "{"; IDENT "measure"; id=IDENT; rel=lconstr; "}" -> (Some (id_of_string id), CMeasureRec rel) | -> (None, CStructRec) ] ] ; diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index bdedaf176..0bd72db4a 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -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") diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index e51b1fecb..613fbfe78 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -384,6 +384,8 @@ let pr_fixdecl pr prd dangling_with_for (id,(n,ro),bl,t,c) = else mt() | CWfRec c -> spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}" + | CMeasureRec c -> + spc () ++ str "{measure " ++ pr lsimple c ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}" in pr_recursive_decl pr prd dangling_with_for id bl annot t c diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index c50b2e52f..b181247ab 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -572,6 +572,9 @@ let rec pr_vernac = function | CWfRec c -> spc() ++ str "{wf " ++ pr_name name ++ spc() ++ pr_lconstr_expr c ++ str"}" + | CMeasureRec c -> + spc() ++ str "{measure " ++ pr_name name ++ spc() ++ + pr_lconstr_expr c ++ str"}" in pr_id id ++ pr_binders_arg bl ++ annot ++ spc() ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_ |