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/vernacexpr.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/vernacexpr.ml')
| -rw-r--r-- | vernac/vernacexpr.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 8b8123bd30..6f09d9a39b 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -131,7 +131,8 @@ type definition_expr = type decl_notation = lstring * constr_expr * scope_name option type 'a fix_expr_gen = - { id_decl : ident_decl + { fname : lident + ; univs : universe_decl_expr option ; rec_order : 'a ; binders : local_binder_expr list ; rtype : constr_expr |