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.

3 files changed, 16 insertions, 15 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 0ae3de7321..4dc3ba8789 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -399,12 +399,12 @@ let tag_var = tag Tag.variable
       pr_opt_type_spc pr t ++ str " :=" ++
       pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c
 
-  let pr_guard_annot pr_aux bl (n,ro) =
-    match n with
+  let pr_guard_annot pr_aux bl ro =
+    match ro with
       | None -> mt ()
-      | Some {loc; v = id} ->
+      | Some {loc; v = ro} ->
         match (ro : Constrexpr.recursion_order_expr) with
-          | CStructRec ->
+          | CStructRec { v = id } ->
             let names_of_binder = function
               | CLocalAssum (nal,_,_) -> nal
               | CLocalDef (_,_,_) -> []
@@ -413,10 +413,11 @@ let tag_var = tag Tag.variable
                if List.length ids > 1 then
                  spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}"
                else mt()
-          | CWfRec c ->
-            spc() ++ str "{" ++ keyword "wf" ++ spc () ++ pr_aux c ++ spc() ++ pr_id id ++ str"}"
-          | CMeasureRec (m,r) ->
-            spc() ++ str "{" ++ keyword "measure" ++ spc () ++ pr_aux m ++ spc() ++ pr_id id++
+          | CWfRec (id,c) ->
+            spc() ++ str "{" ++ keyword "wf" ++ spc () ++ pr_aux c ++ spc() ++ pr_lident id ++ str"}"
+          | CMeasureRec (id,m,r) ->
+            spc() ++ str "{" ++ keyword "measure" ++ spc () ++ pr_aux m ++
+            match id with None -> mt() | Some id -> spc () ++ pr_lident id ++
               (match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}"
 
   let pr_fixdecl pr prd dangling_with_for ({v=id},ro,bl,t,c) =
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index db1687a49b..2e00b12899 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -37,7 +37,7 @@ val pr_glob_level : Glob_term.glob_level -> Pp.t
 val pr_glob_sort : Glob_term.glob_sort -> Pp.t
 val pr_guard_annot : (constr_expr -> Pp.t) ->
   local_binder_expr list ->
-  lident option * recursion_order_expr ->
+  recursion_order_expr CAst.t option ->
   Pp.t
 
 val pr_record_body : (qualid * constr_expr) list -> Pp.t
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