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 /interp/constrexpr.ml | |
| 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 'interp/constrexpr.ml')
| -rw-r--r-- | interp/constrexpr.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index 7a14a4e708..653bb68f30 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -134,16 +134,16 @@ and branch_expr = (cases_pattern_expr list list * constr_expr) CAst.t and fix_expr = - lident * (lident option * recursion_order_expr) * + lident * (recursion_order_expr CAst.t) option * local_binder_expr list * constr_expr * constr_expr and cofix_expr = lident * local_binder_expr list * constr_expr * constr_expr and recursion_order_expr = - | CStructRec - | CWfRec of constr_expr - | CMeasureRec of constr_expr * constr_expr option (** measure, relation *) + | CStructRec of lident + | CWfRec of lident * constr_expr + | CMeasureRec of lident option * constr_expr * constr_expr option (** argument, measure, relation *) (* Anonymous defs allowed ?? *) and local_binder_expr = |