diff options
| author | Pierre-Marie Pédrot | 2020-06-23 11:14:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-23 17:00:44 +0200 |
| commit | 93e7eff5e55be0b6ddc68cd90a175e38793c6b62 (patch) | |
| tree | 78c464dec10231875926a684b908803c608b2e90 /tactics | |
| parent | 25ece321f2297bd28971be3df2616626a7de9516 (diff) | |
Correctly classify variables as being unfoldable in dnet patterns.
Fixes #12571.
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 |