diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/rawterm.ml | 3 | ||||
| -rw-r--r-- | pretyping/rawterm.mli | 2 |
2 files changed, 5 insertions, 0 deletions
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 78425e107a..6442ca9693 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -324,6 +324,9 @@ type 'a raw_red_flag = { rConst : 'a list } +let all_flags = + {rBeta = true; rIota = true; rZeta = true; rDelta = true; rConst = []} + type 'a occurrences = int list * 'a type ('a,'b) red_expr_gen = diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 651530c94c..869861ccd7 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -117,6 +117,8 @@ type 'a raw_red_flag = { rConst : 'a list } +val all_flags : 'a raw_red_flag + type 'a occurrences = int list * 'a type ('a,'b) red_expr_gen = |