diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/genredexpr.ml | 13 |
1 files 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 |