From b7ec355d3af240519cde9660dd2562b93f87c555 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 10 Dec 2020 17:33:55 +0100
Subject: Generalize the type of red_expr w.r.t. the type of flags they
 contain.

---
 tactics/genredexpr.ml | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/tactics/genredexpr.ml b/tactics/genredexpr.ml
index 1f6b04c1d3..9939490e79 100644
--- a/tactics/genredexpr.ml
+++ b/tactics/genredexpr.ml
@@ -35,13 +35,13 @@ type 'a glob_red_flag = {
 
 (** Generic kinds of reductions *)
 
-type ('a,'b,'c) red_expr_gen =
+type ('a, 'b, 'c, 'flags) red_expr_gen0 =
   | Red of bool
   | Hnf
-  | Simpl of 'b glob_red_flag*('b,'c) Util.union Locus.with_occurrences option
-  | Cbv of 'b glob_red_flag
-  | Cbn of 'b glob_red_flag
-  | Lazy of 'b glob_red_flag
+  | Simpl of 'flags * ('b, 'c) Util.union Locus.with_occurrences option
+  | Cbv of 'flags
+  | Cbn of 'flags
+  | Lazy of 'flags
   | Unfold of 'b Locus.with_occurrences list
   | Fold of 'a list
   | Pattern of 'a Locus.with_occurrences list
@@ -49,6 +49,9 @@ type ('a,'b,'c) red_expr_gen =
   | CbvVm of ('b,'c) Util.union Locus.with_occurrences option
   | CbvNative of ('b,'c) Util.union Locus.with_occurrences option
 
+type ('a, 'b, 'c) red_expr_gen =
+  ('a, 'b, 'c, 'b glob_red_flag) red_expr_gen0
+
 type ('a,'b,'c) may_eval =
   | ConstrTerm of 'a
   | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
-- 
cgit v1.2.3