diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacexpr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 428c674754..b37460e483 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -27,7 +27,7 @@ type split_flag = bool (* true = exists false = split *) type hidden_flag = bool (* true = internal use false = user-level *) type letin_flag = bool (* true = use local def false = use Leibniz *) -type raw_red_flag = +type glob_red_flag = | FBeta | FIota | FZeta |