diff options
| author | Gaëtan Gilbert | 2020-07-02 14:41:38 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-02 14:41:38 +0200 |
| commit | a1835c755f07b2199d122632360a5d236cd9984e (patch) | |
| tree | 747a3d537e26342c1fed3246aff2ba01ee27de8e /tactics | |
| parent | e04fbe4eb39434f50cf6bdf19f6c4be46b73ef44 (diff) | |
| parent | 93e7eff5e55be0b6ddc68cd90a175e38793c6b62 (diff) | |
Merge PR #12572: Correctly classify variables as being unfoldable in dnet patterns.
Reviewed-by: SkySkimmer
Reviewed-by: maximedenes
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/btermdn.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index 6e6af42010..3bed329d31 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -77,7 +77,7 @@ let constr_val_discr_st sigma ts t = | Const (c,u) -> if TransparentState.is_transparent_constant ts c then Everything else Label(GRLabel (ConstRef c),l) | Ind (ind_sp,u) -> Label(GRLabel (IndRef ind_sp),l) | Construct (cstr_sp,u) -> Label(GRLabel (ConstructRef cstr_sp),l) - | Var id when not (TransparentState.is_transparent_variable ts id) -> Label(GRLabel (VarRef id),l) + | Var id -> if TransparentState.is_transparent_variable ts id then Everything else Label(GRLabel (VarRef id),l) | Prod (n, d, c) -> Label(ProdLabel, [d; c]) | Lambda (n, d, c) -> if List.is_empty l then @@ -85,7 +85,8 @@ let constr_val_discr_st sigma ts t = else Everything | Sort _ -> Label(SortLabel, []) | Evar _ -> Everything - | _ -> Nothing + | Rel _ | Meta _ | Cast _ | LetIn _ | App _ | Case _ | Fix _ | CoFix _ + | Proj _ | Int _ | Float _ -> Nothing let constr_pat_discr_st ts t = let open GlobRef in |