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.

1 files changed, 6 insertions, 6 deletions

diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index d042a1d650..f378a5d2dd 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -438,18 +438,18 @@ let match_goals ot nt =
       | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (2)")
     in
     let recursion_order_expr ogname exp exp2 =
-      match exp, exp2 with
-      | CStructRec, CStructRec -> ()
-      | CWfRec c, CWfRec c2 ->
+      match exp.CAst.v, exp2.CAst.v with
+      | CStructRec _, CStructRec _ -> ()
+      | CWfRec (_,c), CWfRec (_,c2) ->
         constr_expr ogname c c2
-      | CMeasureRec (m,r), CMeasureRec (m2,r2) ->
+      | CMeasureRec (_,m,r), CMeasureRec (_,m2,r2) ->
         constr_expr ogname m m2;
         constr_expr_opt ogname r r2
       | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (3)")
     in
     let fix_expr ogname exp exp2 =
-      let (l,(lo,ro),lb,ce1,ce2), (l2,(lo2,ro2),lb2,ce12,ce22) = exp,exp2 in
-        recursion_order_expr ogname ro ro2;
+      let (l,ro,lb,ce1,ce2), (l2,ro2,lb2,ce12,ce22) = exp,exp2 in
+        Option.iter2 (recursion_order_expr ogname) ro ro2;
         iter2 (local_binder_expr ogname) lb lb2;
         constr_expr ogname ce1 ce12;
         constr_expr ogname ce2 ce22