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 | |
| parent | e04fbe4eb39434f50cf6bdf19f6c4be46b73ef44 (diff) | |
| parent | 93e7eff5e55be0b6ddc68cd90a175e38793c6b62 (diff) | |
Merge PR #12572: Correctly classify variables as being unfoldable in dnet patterns.
Reviewed-by: SkySkimmer
Reviewed-by: maximedenes
| -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. |