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/notation_ops.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/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 9801e56ca1..7f084fffdd 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -957,7 +957,7 @@ let match_fix_kind fk1 fk2 = match (fk1,fk2) with | GCoFix n1, GCoFix n2 -> Int.equal n1 n2 | GFix (nl1,n1), GFix (nl2,n2) -> - let test (n1, _) (n2, _) = match n1, n2 with + let test n1 n2 = match n1, n2 with | _, None -> true | Some id1, Some id2 -> Int.equal id1 id2 | _ -> false |