diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 17 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 18 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 | ||||
| -rw-r--r-- | parsing/ppconstr.ml | 19 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 13 |
5 files changed, 33 insertions, 36 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 41f89a541d..277d8b3c8c 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -43,12 +43,11 @@ let loc_of_binder_let = function let rec index_and_rec_order_of_annot loc bl ann = match names_of_local_assums bl,ann with - | [_], (None, r) -> Some 0, r - | lids, (Some x, ro) -> - let ids = List.map snd lids in - (try Some (list_index0 (snd x) ids), ro - with Not_found -> - user_err_loc(fst x,"index_of_annot", Pp.str"no such fix variable")) + | [loc,Name id], (None, r) -> Some (loc, id), r + | lids, (Some (loc, n), ro) -> + if List.exists (fun (_, x) -> x = Name n) lids then + Some (loc, n), ro + else user_err_loc(loc,"index_of_annot", Pp.str"no such fix variable") | _, (None, r) -> None, r let mk_fixb (id,bl,ann,body,(loc,tyc)) = @@ -370,9 +369,9 @@ GEXTEND Gram ] ] ; fixannot: - [ [ "{"; IDENT "struct"; id=name; "}" -> (Some id, CStructRec) - | "{"; IDENT "wf"; rel=constr; id=OPT name; "}" -> (id, CWfRec rel) - | "{"; IDENT "measure"; rel=constr; id=OPT name; "}" -> (id, CMeasureRec rel) + [ [ "{"; IDENT "struct"; id=identref; "}" -> (Some id, CStructRec) + | "{"; IDENT "wf"; rel=constr; id=OPT identref; "}" -> (id, CWfRec rel) + | "{"; IDENT "measure"; rel=constr; id=OPT identref; "}" -> (id, CMeasureRec rel) ] ] ; binders_let_fixannot: diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 8285bbad37..76646a4f97 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -263,18 +263,22 @@ GEXTEND Gram ty = type_cstr; ":="; def = lconstr; ntn = decl_notation -> let bl, annot = (b :: fst bl, snd bl) in - let names = List.map snd (names_of_local_assums bl) in + let names = names_of_local_assums bl in let ni = match fst annot with - Some (_, id) -> - (try Some (list_index0 id names) - with Not_found -> Util.user_err_loc - (loc,"Fixpoint", - Pp.str "No argument named " ++ Nameops.pr_name id)) + Some (loc, id) -> + (if List.exists (fun (_, id') -> Name id = id') names then + Some (loc, id) + else Util.user_err_loc + (loc,"Fixpoint", + Pp.str "No argument named " ++ Nameops.pr_id id)) | None -> (* 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 + if List.length names = 1 then + let (loc, na) = List.hd names in + Some (loc, Nameops.out_name na) + else None in ((id,(ni,snd annot),bl,ty,def),ntn) ] ] ; diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index d9d4139e95..6f6cff2752 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -166,7 +166,7 @@ module Constr : val binder_let : local_binder Gram.Entry.e val delimited_binder_let : local_binder Gram.Entry.e val binders_let : local_binder list Gram.Entry.e - val binders_let_fixannot : (local_binder list * (name located option * recursion_order_expr)) Gram.Entry.e + val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e val delimited_binders_let : local_binder list Gram.Entry.e val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 21c5a343b4..41d98f2bc8 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -395,16 +395,15 @@ let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c = let pr_fixdecl pr prd dangling_with_for (id,(n,ro),bl,t,c) = let annot = - let ids = names_of_local_assums bl in - match ro with - CStructRec -> - if List.length ids > 1 && n <> None then - spc() ++ str "{struct " ++ pr_name (snd (List.nth ids (Option.get n))) ++ str"}" - else mt() - | CWfRec c -> - spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids (Option.get n))) ++ str"}" - | CMeasureRec c -> - spc () ++ str "{measure " ++ pr lsimple c ++ pr_name (snd (List.nth ids (Option.get n))) ++ str"}" + match ro with + CStructRec -> + if List.length bl > 1 && n <> None then + spc() ++ str "{struct " ++ pr_id (snd (Option.get n)) ++ str"}" + else mt() + | CWfRec c -> + spc () ++ str "{wf " ++ pr lsimple c ++ pr_id (snd (Option.get n)) ++ str"}" + | CMeasureRec c -> + spc () ++ str "{measure " ++ pr lsimple c ++ pr_id (snd (Option.get 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 57e21c2ce6..352f58f6ba 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -594,23 +594,18 @@ let rec pr_vernac = function let annot = 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 + | Some (loc, id) -> match (ro : Topconstr.recursion_order_expr) with CStructRec -> if List.length ids > 1 then - spc() ++ str "{struct " ++ pr_name name ++ str"}" + spc() ++ str "{struct " ++ pr_id id ++ str"}" else mt() | CWfRec c -> spc() ++ str "{wf " ++ pr_lconstr_expr c ++ spc() ++ - pr_name name ++ str"}" + pr_id id ++ str"}" | CMeasureRec c -> spc() ++ str "{measure " ++ pr_lconstr_expr c ++ spc() ++ - pr_name name ++ str"}" + pr_id id ++ str"}" in pr_id id ++ pr_binders_arg bl ++ annot ++ spc() ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_ |