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 | |
| parent | 25ece321f2297bd28971be3df2616626a7de9516 (diff) | |
Correctly classify variables as being unfoldable in dnet patterns.
Fixes #12571.
| -rw-r--r-- | doc/changelog/04-tactics/12572-fix-12571.rst | 6 | ||||
| -rw-r--r-- | tactics/btermdn.ml | 5 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_12571.v | 20 |
3 files changed, 29 insertions, 2 deletions
diff --git a/doc/changelog/04-tactics/12572-fix-12571.rst b/doc/changelog/04-tactics/12572-fix-12571.rst new file mode 100644 index 0000000000..98b217e86b --- /dev/null +++ b/doc/changelog/04-tactics/12572-fix-12571.rst @@ -0,0 +1,6 @@ +- **Fixed:** + typeclasses eauto (and discriminated hint bases) now correctly + classify local variables as being unfoldable + (`#12572 <https://github.com/coq/coq/pull/12572>`_, + fixes `#12571 <https://github.com/coq/coq/issues/12571>`_, + by Pierre-Marie Pédrot). 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 diff --git a/test-suite/bugs/closed/bug_12571.v b/test-suite/bugs/closed/bug_12571.v new file mode 100644 index 0000000000..c348626921 --- /dev/null +++ b/test-suite/bugs/closed/bug_12571.v @@ -0,0 +1,20 @@ +Axiom IsTrunc : Type -> Type. + +Existing Class IsTrunc. + +Declare Instance trunc_forall : + forall (A : Type) (P : A -> Type), + IsTrunc (forall a : A, P a). + +Axiom Graph : Set. +Axiom in_N : forall (n : Graph), Type. + +Definition N : Type := @sigT Graph in_N. + +Goal forall (P : N -> Type) + (Q := fun m : Graph => forall mrec : in_N m, P (existT _ m mrec)) + (A : Graph), IsTrunc (Q A). +Proof. +intros. +solve [typeclasses eauto]. +Qed. |