[go: up one dir, main page]
Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

rm problematic variables under beta redexes for evar instantiation #19833

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

rm problematic variables under beta redexes for evar instantiation #19833

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
7f21d39
rm problematic variables under beta redexes for evar instantiation
Tragicus Nov 7, 2024
4477d89
changelog and test-suite example
Tragicus Nov 17, 2024
114cf23
changelog msg
Tragicus Nov 17, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions doc/changelog/02-specification-language/19833-evd-inst-beta.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
- **Changed:**
Unification will now reduce beta-redexes when necessary to instantiate evars
(`#19833 <https://github.com/coq/coq/pull/19833>`_,
by Quentin Vermande).
7 changes: 7 additions & 0 deletions pretyping/evarsolve.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1746,6 +1746,13 @@ let rec invert_definition unify flags choose imitate_defs
add_conv_oriented_pb (None,env',mkEvar ev'',mkEvar ev') evd in
evdref := evd;
evar'')
| App (f, args) when EConstr.isLambda !evdref f ->
let p = !progress in
progress := true;
(try
map_constr_with_full_binders env' !evdref (fun d (env,k) -> push_rel d env, k+1)
imitate envk t
with _ -> progress := p; imitate envk (whd_beta env' !evdref t))
| _ ->
progress := true;
match
Expand Down
22 changes: 22 additions & 0 deletions test-suite/bugs/bug_19833.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
Class hasPt (T : Type) := Pt { pt_ : T }.
Structure ptType := Pointed {
sort :> Type;
class : hasPt sort
}.

Definition pt (T : ptType) := @pt_ T (class T).

Canonical nat_ptType := Pointed nat (Pt nat 0).
Canonical forall_ptType (T : Type) (U : T -> ptType) :=
Pointed (forall t, U t) (Pt (forall t, U t) (fun t => pt (U t))).

Definition constant {T U : Type} (f : T -> U) := forall (x y : T), f x = f y.
Definition cst (T U : Type) (y : U) := fun _ : T => y.
Lemma constant_cst (T U : Type) (y : U) : constant (cst T U y).
Proof. intros x x'; reflexivity. Qed.

Goal forall {T : Type} {U : ptType}, constant (pt (T -> U)).
Proof.
intros.
exact (constant_cst _ _ _).
Qed.
Loading