diff options
| author | Maxime Dénès | 2018-12-07 13:38:59 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-16 18:45:32 +0200 |
| commit | 414cfd64702be920c9d96514e3802bc950b5ea0b (patch) | |
| tree | bdc7e8eca2b50da60d1a893124a9c93aea9d1841 /printing/ppconstr.mli | |
| parent | 4b9119d8090e366ecd2e803ad30a9dd839bc8ec9 (diff) | |
Clean the representation of recursive annotation in Constrexpr
We make clearer which arguments are optional and which are mandatory.
Some of these representations are tricky because of small differences
between Program and Function, which share the same infrastructure.
As a side-effect of this cleanup, Program Fixpoint can now be used with
e.g. {measure (m + n) R}. Previously, parentheses were required around
R.
Diffstat (limited to 'printing/ppconstr.mli')
| -rw-r--r-- | printing/ppconstr.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index db1687a49b..2e00b12899 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -37,7 +37,7 @@ val pr_glob_level : Glob_term.glob_level -> Pp.t val pr_glob_sort : Glob_term.glob_sort -> Pp.t val pr_guard_annot : (constr_expr -> Pp.t) -> local_binder_expr list -> - lident option * recursion_order_expr -> + recursion_order_expr CAst.t option -> Pp.t val pr_record_body : (qualid * constr_expr) list -> Pp.t |