diff options
| author | Emilio Jesus Gallego Arias | 2019-07-19 18:55:05 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-23 14:31:10 +0200 |
| commit | d407d1f3f2f877fca8673eaf0470b3390e55dbaa (patch) | |
| tree | 5493ae8ba45ef916d14c1e90d722da2aadf801c0 /vernac/ppvernac.ml | |
| parent | d68f695b5a953c50bcf5e80182ef317682de1a05 (diff) | |
[vernacexpr] Remove duplicate fixpoint record.
We continue over the previous commit and remove redundant
`structured_fixpoint_expr` record in favor of the one used in the AST.
This removes some term-shuffling, tho we still have discrepancies
related to adjustments on the recursive annotation.
Diffstat (limited to 'vernac/ppvernac.ml')
| -rw-r--r-- | vernac/ppvernac.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 835f5e0b75..e25118e0a8 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -419,12 +419,12 @@ let string_of_theorem_kind = let open Decls in function | l -> spc() ++ hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")") - let pr_rec_definition { id_decl; rec_order; binders; rtype; body_def; notations } = + let pr_rec_definition { fname; univs; rec_order; binders; rtype; body_def; notations } = let env = Global.env () in let sigma = Evd.from_env env in let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in let annot = pr_guard_annot (pr_lconstr_expr env sigma) binders rec_order in - pr_ident_decl id_decl ++ pr_binders_arg binders ++ annot + pr_ident_decl (fname,univs) ++ pr_binders_arg binders ++ annot ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr env sigma c) rtype ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr env sigma def) body_def ++ prlist (pr_decl_notation @@ pr_constr env sigma) notations @@ -858,8 +858,8 @@ let string_of_definition_object_kind = let open Decls in function | DoDischarge -> keyword "Let" ++ spc () | NoDischarge -> str "" in - let pr_onecorec {id_decl; binders; rtype; body_def; notations } = - pr_ident_decl id_decl ++ spc() ++ pr_binders env sigma binders ++ spc() ++ str":" ++ + let pr_onecorec {fname; univs; binders; rtype; body_def; notations } = + pr_ident_decl (fname,univs) ++ spc() ++ pr_binders env sigma binders ++ spc() ++ str":" ++ spc() ++ pr_lconstr_expr env sigma rtype ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr env sigma def) body_def ++ prlist (pr_decl_notation @@ pr_constr env sigma) notations |