From 414cfd64702be920c9d96514e3802bc950b5ea0b Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 7 Dec 2018 13:38:59 +0100
Subject: 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.
---
 interp/notation_ops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation_ops.ml')

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
-- 
cgit v1.2.3