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.
---
 printing/proof_diffs.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'printing/proof_diffs.ml')

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