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_term.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation_term.ml')

diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 6fe20486dc..5024f5c26f 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -38,7 +38,7 @@ type notation_constr =
       notation_constr * notation_constr
   | NIf of notation_constr * (Name.t * notation_constr option) *
       notation_constr * notation_constr
-  | NRec of fix_kind * Id.t array *
+  | NRec of glob_fix_kind * Id.t array *
       (Name.t * notation_constr option * notation_constr) list array *
       notation_constr array * notation_constr array
   | NSort of glob_sort
-- 
cgit v1.2.3