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 /vernac/comFixpoint.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 'vernac/comFixpoint.mli')
| -rw-r--r-- | vernac/comFixpoint.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 15ff5f4498..5937842f17 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -62,7 +62,7 @@ val interp_recursive : (** Extracting the semantical components out of the raw syntax of (co)fixpoints declarations *) -val extract_fixpoint_components : bool -> +val extract_fixpoint_components : structonly:bool -> (fixpoint_expr * decl_notation list) list -> structured_fixpoint_expr list * decl_notation list |