diff options
| author | Pierre-Marie Pédrot | 2020-12-10 17:33:55 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-12 14:27:30 +0100 |
| commit | b7ec355d3af240519cde9660dd2562b93f87c555 (patch) | |
| tree | d1206321761c1566c56f49f6aac530e782abbd87 /tactics | |
| parent | 233629e8f6e40057a8caf7502047995427740ae8 (diff) | |
Generalize the type of red_expr w.r.t. the type of flags they contain.
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 |