[ast] [constrexpr] Make recursion_order_expr an AST node.

This is a bit more uniform.

7 files changed, 19 insertions, 15 deletions

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 653bb68f30..9f778d99e9 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -134,16 +134,17 @@ and branch_expr =
   (cases_pattern_expr list list * constr_expr) CAst.t
 
 and fix_expr =
-    lident * (recursion_order_expr CAst.t) option *
+    lident * recursion_order_expr option *
       local_binder_expr list * constr_expr * constr_expr
 
 and cofix_expr =
     lident * local_binder_expr list * constr_expr * constr_expr
 
-and recursion_order_expr =
+and recursion_order_expr_r =
   | CStructRec of lident
   | CWfRec of lident * constr_expr
   | CMeasureRec of lident option * constr_expr * constr_expr option (** argument, measure, relation *)
+and recursion_order_expr = recursion_order_expr_r CAst.t
 
 (* Anonymous defs allowed ?? *)
 and local_binder_expr =
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index db860e0c3b..443473d5b6 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -198,7 +198,7 @@ and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} =
 
 and fix_expr_eq (id1,r1,bl1,a1,b1) (id2,r2,bl2,a2,b2) =
   (eq_ast Id.equal id1 id2) &&
-  Option.equal (eq_ast recursion_order_expr_eq) r1 r2 &&
+  Option.equal recursion_order_expr_eq r1 r2 &&
   List.equal local_binder_eq bl1 bl2 &&
   constr_expr_eq a1 a2 &&
   constr_expr_eq b1 b2
@@ -209,7 +209,7 @@ and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) =
   constr_expr_eq a1 a2 &&
   constr_expr_eq b1 b2
 
-and recursion_order_expr_eq r1 r2 = match r1, r2 with
+and recursion_order_expr_eq_r r1 r2 = match r1, r2 with
   | CStructRec i1, CStructRec i2 -> eq_ast Id.equal i1 i2
   | CWfRec (i1,e1), CWfRec (i2,e2) ->
     constr_expr_eq e1 e2
@@ -218,6 +218,8 @@ and recursion_order_expr_eq r1 r2 = match r1, r2 with
     constr_expr_eq e1 e2 && Option.equal constr_expr_eq o1 o2
   | _ -> false
 
+and recursion_order_expr_eq r1 r2 = eq_ast recursion_order_expr_eq_r r1 r2
+
 and local_binder_eq l1 l2 = match l1, l2 with
   | CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) ->
     eq_ast Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 7786155092..4a9190c10a 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -440,10 +440,10 @@ GRAMMAR EXTEND Gram
     ] ]
   ;
   fixannot:
-    [ [ "{"; IDENT "struct"; id=identref; "}" -> { CStructRec id }
-    | "{"; IDENT "wf"; rel=constr; id=identref; "}" -> { CWfRec(id,rel) }
+    [ [ "{"; IDENT "struct"; id=identref; "}" -> { CAst.make ~loc @@ CStructRec id }
+    | "{"; IDENT "wf"; rel=constr; id=identref; "}" -> { CAst.make ~loc @@ CWfRec(id,rel) }
     | "{"; IDENT "measure"; m=constr; id=OPT identref;
-        rel=OPT constr; "}" -> { CMeasureRec (id,m,rel) }
+        rel=OPT constr; "}" -> { CAst.make ~loc @@ CMeasureRec (id,m,rel) }
     ] ]
   ;
   impl_name_head:
@@ -452,7 +452,7 @@ GRAMMAR EXTEND Gram
   binders_fixannot:
     [ [ na = impl_name_head; assum = impl_ident_tail; bl = binders_fixannot ->
           { (assum na :: fst bl), snd bl }
-      | f = fixannot -> { [], Some (CAst.make ~loc f) }
+      | f = fixannot -> { [], Some f }
       | b = binder; bl = binders_fixannot -> { b @ fst bl, snd bl }
       | -> { [], None }
     ] ]
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 84d19730fa..3a57c14a3b 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -191,7 +191,7 @@ module Constr :
     val binder : local_binder_expr list Entry.t (* closed_binder or variable *)
     val binders : local_binder_expr list Entry.t (* list of binder *)
     val open_binders : local_binder_expr list Entry.t
-    val binders_fixannot : (local_binder_expr list * recursion_order_expr CAst.t option) Entry.t
+    val binders_fixannot : (local_binder_expr list * recursion_order_expr option) Entry.t
     val typeclass_constraint : (lname * bool * constr_expr) Entry.t
     val record_declaration : constr_expr Entry.t
     val appl_arg : (constr_expr * explicitation CAst.t option) Entry.t
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 4dc3ba8789..78733784a7 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -403,7 +403,7 @@ let tag_var = tag Tag.variable
     match ro with
       | None -> mt ()
       | Some {loc; v = ro} ->
-        match (ro : Constrexpr.recursion_order_expr) with
+        match ro with
           | CStructRec { v = id } ->
             let names_of_binder = function
               | CLocalAssum (nal,_,_) -> nal
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 2e00b12899..1332cd0168 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -35,10 +35,11 @@ val pr_patvar : Pattern.patvar -> Pp.t
 
 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 ->
-  recursion_order_expr CAst.t option ->
-  Pp.t
+val pr_guard_annot
+  :  (constr_expr -> Pp.t)
+  -> local_binder_expr list
+  -> recursion_order_expr option
+  -> Pp.t
 
 val pr_record_body : (qualid * constr_expr) list -> Pp.t
 val pr_binders : Environ.env -> Evd.evar_map -> local_binder_expr list -> Pp.t
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 8eacaed2eb..c8ccd699ac 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -129,7 +129,7 @@ type definition_expr =
       * constr_expr option
 
 type fixpoint_expr =
-    ident_decl * recursion_order_expr CAst.t option * local_binder_expr list * constr_expr * constr_expr option
+    ident_decl * recursion_order_expr option * local_binder_expr list * constr_expr * constr_expr option
 
 type cofixpoint_expr =
     ident_decl * local_binder_expr list * constr_expr * constr_expr option