diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 7 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 17 | ||||
| -rw-r--r-- | parsing/g_xml.ml4 | 4 | ||||
| -rw-r--r-- | parsing/ppconstr.ml | 6 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 27 |
5 files changed, 32 insertions, 29 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 9c39878c7d..ed9e1fa06d 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -59,14 +59,13 @@ let rec mkCLambdaN loc bll c = let rec index_and_rec_order_of_annot loc bl ann = match names_of_local_assums bl,ann with - | [_], (None, r) -> 0, r + | [_], (None, r) -> Some 0, r | lids, (Some x, ro) -> let ids = List.map snd lids in - (try list_index (snd x) ids - 1, ro + (try Some (list_index (snd x) ids - 1), ro with Not_found -> user_err_loc(fst x,"index_of_annot", Pp.str"no such fix variable")) - | _ -> user_err_loc(loc,"index_of_annot", - Pp.str "cannot guess decreasing argument of fix") + | _, (None, r) -> None, r let mk_fixb (id,bl,ann,body,(loc,tyc)) = let n,ro = index_and_rec_order_of_annot (fst id) bl ann in diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 87f388a748..0a0df6fb21 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -218,16 +218,15 @@ GEXTEND Gram let ni = match fst annot with Some id -> - (try list_index (Name id) names - 1 - with Not_found -> Util.user_err_loc - (loc,"Fixpoint", - Pp.str "No argument named " ++ Nameops.pr_id id)) + (try Some (list_index (Name id) names - 1) + with Not_found -> Util.user_err_loc + (loc,"Fixpoint", + Pp.str "No argument named " ++ Nameops.pr_id id)) | None -> - if List.length names > 1 then - Util.user_err_loc - (loc,"Fixpoint", - Pp.str "the recursive argument needs to be specified"); - 0 in + (* If there is only one argument, it is the recursive one, + otherwise, we search the recursive index later *) + if List.length names = 1 then Some 0 else None + in ((id, (ni, snd annot), bl, type_, def),ntn) ] ] ; corec_definition: diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 1df3d1f256..8b3661dbe6 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -205,11 +205,11 @@ and interp_xml_recursionOrder x = and interp_xml_FixFunction x = match interp_xml_tag "FixFunction" x with | (loc,al,[x1;x2;x3]) -> - ((nmtoken (get_xml_attr "recIndex" al), + ((Some (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), + ((Some (nmtoken (get_xml_attr "recIndex" al)), RStructRec), (get_xml_ident al, interp_xml_type x1, interp_xml_body x2)) | (loc,_,_) -> user_err_loc (loc,"",str "wrong number of arguments (expect one)") diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index a95fa4bad8..e4cc3cd916 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -379,11 +379,11 @@ let pr_fixdecl pr prd dangling_with_for (id,(n,ro),bl,t,c) = let ids = names_of_local_assums bl in match ro with CStructRec -> - if List.length ids > 1 then - spc() ++ str "{struct " ++ pr_name (snd (List.nth ids n)) ++ str"}" + if List.length ids > 1 && n <> None then + spc() ++ str "{struct " ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}" else mt() | CWfRec c -> - spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids n)) ++ str"}" + spc () ++ str "{wf " ++ 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 c08b076173..f43f93bd90 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -555,18 +555,23 @@ let rec pr_vernac = function else ([],def,type_) in let bl = bl @ bl' in let ids = List.flatten (List.map name_of_binder bl) in - let name = - try snd (List.nth ids n) - with Failure _ -> - warn (str "non-printable fixpoint \""++pr_id id++str"\""); - Anonymous in let annot = - match (ro : Topconstr.recursion_order_expr) with - CStructRec -> - if List.length ids > 1 then - spc() ++ str "{struct " ++ pr_name name ++ str"}" - else mt() - | CWfRec c -> spc() ++ str "{wf " ++ pr_name name ++ spc() ++ pr_lconstr_expr c ++ str"}" + match n with + | None -> mt () + | Some n -> + let name = + try snd (List.nth ids n) + with Failure _ -> + warn (str "non-printable fixpoint \""++pr_id id++str"\""); + Anonymous in + match (ro : Topconstr.recursion_order_expr) with + CStructRec -> + if List.length ids > 1 then + spc() ++ str "{struct " ++ pr_name name ++ str"}" + else mt() + | CWfRec c -> + spc() ++ str "{wf " ++ 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_ |