Add a generic mechanism for rewriting with any equality satisfying J #21098

tabareau · 2025-09-19T14:40:49Z

This PR has a mechanism to rewrite with any equality satisfying reflexivity and the J based typeclass inference.

ppedrot · 2025-09-24T13:43:15Z

@coqbot run full ci

tabareau · 2025-09-25T11:44:51Z

@coqbot run full ci

coqbot-app · 2025-09-29T13:02:37Z

Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/ext_lib/theories/Data/List.v in 14m 27s (from ci-ext_lib) (full log on GitHub Actions - verbose log)

We are collecting data on the user experience of the Coq Bug Minimizer.
If you haven't already filled the survey for this PR, please fill out our short survey!

🌟 Minimized Coq File (consider adding this file to the test-suite)

(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" "-coqlib" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq//" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/ext_lib/theories" "ExtLib" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Stdlib" "Stdlib" "-top" "ExtLib.Data.List") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 263 lines to 26 lines, then from 39 lines to 263 lines, then from 268 lines to 34 lines, then from 48 lines to 34 lines *)
(* coqc version 9.2+alpha compiled with OCaml 4.14.2
   coqtop version 9.2+alpha
   Expected coqc runtime on this file: 0.092 sec *)
Module Export Nat.

Set Implicit Arguments.

Inductive R_nat_lt : nat -> nat -> Prop :=
| R_lt : forall n m, n < m -> R_nat_lt n m.

Theorem wf_R_lt : well_founded R_nat_lt.
Admitted.
Set Universe Polymorphism.
  Inductive R_list_len@{u} {T : Type@{u}} : list T -> list T -> Prop :=
  | R_l_len : forall n m, length n < length m -> R_list_len n m.

  Theorem wf_R_list_len@{u} (T : Type@{u}) : well_founded (@R_list_len T).
  Proof.
    constructor.
intros.
    refine (@Fix _ _ Nat.wf_R_lt (fun n : nat => forall ls : list T, n = length ls -> Acc R_list_len ls)
      (fun x rec ls pfls => Acc_intro _ _)
      _ _ refl_equal).
    refine (
      match ls as ls return x = length ls -> forall z : list T, R_list_len z ls -> Acc R_list_len z with
        | nil => fun (pfls : x = 0) z pf => _
        | cons l ls => fun pfls z pf =>
          rec _ (match pf in R_list_len xs ys return x = length ys -> Nat.R_nat_lt (length xs) x with
                   | R_l_len n m pf' => fun pf_eq => match eq_sym pf_eq in _ = x return Nat.R_nat_lt (length n) x with
                                                     | refl_equal => Nat.R_lt pf'
                                                   end
                 end pfls) _ eq_refl
      end pfls).
    clear - pf; abstract (inversion pf; subst; simpl in *; inversion H).
  Defined.

🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)

🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)

📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 6.0MiB file on GitHub Actions Artifacts under build.log)


-rwxr-xr-x 1 root root  7595368 Sep 29 12:56 votour.orig
++ CI_BUILD_DIR=/github/workspace/builds/coq/coq-failing/_build_ci
++ ls -l /github/workspace/builds/coq/coq-failing/_build_ci
total 8
drwxr-xr-x  7 root root 4096 Sep 29 11:40 ext_lib
drwxr-xr-x 12 root root 4096 Sep 29 11:37 stdlib
++ declare -A overlays
++ set +x
+ git_download ext_lib
+ local project=ext_lib
+ local dest=/github/workspace/builds/coq/coq-failing/_build_ci/ext_lib
+ local giturl_var=ext_lib_CI_GITURL
+ local giturl=https://github.com/coq-community/coq-ext-lib
+ local ref_var=ext_lib_CI_REF
+ local ref=master
+ local parent_project_var=ext_lib_CI_PARENT_PROJECT
+ local parent_project=
+ local submodule_folder_var=ext_lib_CI_SUBMODULE_FOLDER
+ local submodule_folder=
+ local ov_url=
+ local ov_ref=
++ dirname /github/workspace/builds/coq/coq-failing/_build_ci/ext_lib
+ local dest_prefix=/github/workspace/builds/coq/coq-failing/_build_ci/
+ '[' '' = '' ']'
+ local parent_project_dest=/github/workspace/builds/coq/coq-failing/_build_ci/
+ local parent_project_relative_dest=
+ '[' -d /github/workspace/builds/coq/coq-failing/_build_ci/ext_lib ']'
+ echo 'Warning: download and unpacking of ext_lib skipped because /github/workspace/builds/coq/coq-failing/_build_ci/ext_lib already exists.'
Warning: download and unpacking of ext_lib skipped because /github/workspace/builds/coq/coq-failing/_build_ci/ext_lib already exists.
+ '[' '' ']'
+ cd /github/workspace/builds/coq/coq-failing/_build_ci/ext_lib
+ make
+ '[' -z '' ']'
+ '[' -n 2 ']'
+ command make -j 2
make -f Makefile.coq
make[1]: Entering directory '/github/workspace/builds/coq/coq-failing/_build_ci/ext_lib'
ROCQ compile theories/Data/Member.v
ROCQ compile theories/Data/List.v
MINIMIZER_DEBUG_EXTRA: coqc: /github/workspace/builds/coq/coq-failing/_install_ci/bin/////rocq
MINIMIZER_DEBUG_EXTRA: coqc: /github/workspace/builds/coq/coq-failing/_install_ci/bin/////rocq
MINIMIZER_DEBUG_EXTRA: original invocation: compile -q -w -deprecated-native-compiler-option -native-compiler ondemand -Q theories ExtLib theories/Data/List.v 
MINIMIZER_DEBUG_EXTRA: original invocation: compile -q -w -deprecated-native-compiler-option -native-compiler ondemand -Q theories ExtLib theories/Data/Member.v 
MINIMIZER_DEBUG_EXTRA: new invocation: /github/workspace/builds/coq/coq-failing/_install_ci/bin/rocq.orig compile -q -w -deprecated-native-compiler-option -native-compiler ondemand -Q /github/workspace/builds/coq/coq-failing/_build_ci/ext_lib/theories ExtLib theories/Data/Member.v 
MINIMIZER_DEBUG_EXTRA: new invocation: /github/workspace/builds/coq/coq-failing/_install_ci/bin/rocq.orig compile -q -w -deprecated-native-compiler-option -native-compiler ondemand -Q /github/workspace/builds/coq/coq-failing/_build_ci/ext_lib/theories ExtLib theories/Data/List.v 
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: coqpath: 
MINIMIZER_DEBUG_EXTRA: ocamlpath: /github/workspace/builds/coq/coq-failing/_install_ci/lib:
MINIMIZER_DEBUG_EXTRA: ocamlpath: /github/workspace/builds/coq/coq-failing/_install_ci/lib:
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/builds/coq/coq-failing/_build_ci/ext_lib
MINIMIZER_DEBUG_EXTRA: pwd: PWD=/github/workspace/builds/coq/coq-failing/_build_ci/ext_lib
MINIMIZER_DEBUG_EXTRA: exec: /github/workspace/builds/coq/coq-failing/_install_ci/bin/rocq.orig compile -q -w -deprecated-native-compiler-option -native-compiler ondemand -Q /github/workspace/builds/coq/coq-failing/_build_ci/ext_lib/theories ExtLib theories/Data/Member.v 
MINIMIZER_DEBUG_EXTRA: exec: /github/workspace/builds/coq/coq-failing/_install_ci/bin/rocq.orig compile -q -w -deprecated-native-compiler-option -native-compiler ondemand -Q /github/workspace/builds/coq/coq-failing/_build_ci/ext_lib/theories ExtLib theories/Data/List.v 
MINIMIZER_DEBUG_EXTRA: coqlib: Warning: Deprecated environment variable COQLIB, use ROCQLIB instead.
/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq//
MINIMIZER_DEBUG_EXTRA: coqlib: Warning: Deprecated environment variable COQLIB, use ROCQLIB instead.
/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq//
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.zqUnTiwaZe
MINIMIZER_DEBUG: info: /tmp/tmp-coqbot-minimizer.jmjgO44UVE
MINIMIZER_DEBUG: files:  theories/Data/List.v /github/workspace/builds/coq/coq-failing/_build_ci/ext_lib/theories/Data/List.v
MINIMIZER_DEBUG: files:  theories/Data/Member.v /github/workspace/builds/coq/coq-failing/_build_ci/ext_lib/theories/Data/Member.v
Warning, feedback message received but no listener to handle it!
Warning: Deprecated environment variable COQLIB, use ROCQLIB instead.
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]Warning, feedback message received but no listener to handle it!
Warning, feedback message received but no listener to handle it!
Warning: Deprecated environment variable COQLIB, use ROCQLIB instead.
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]Warning, feedback message received but no listener to handle it!
Warning: Deprecated environment variable COQLIB, use ROCQLIB instead.
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
Warning: Deprecated environment variable COQCORELIB,
use ROCQRUNTIMELIB instead.
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
Warning: Deprecated environment variable COQLIB, use ROCQLIB instead.
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
Warning: Deprecated environment variable COQCORELIB,
use ROCQRUNTIMELIB instead.
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
File "./theories/Data/Member.v", line 2, characters 0-30:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./theories/Data/List.v", line 1, characters 0-38:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./theories/Data/Member.v", line 3, characters 15-24:
Warning: Loading Stdlib without prefix is deprecated.
Use "From Stdlib Require Relations"
or the deprecated "From Coq Require Relations"
for compatibility with older Coq versions.
[deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
theories/Data/Member.vo (real: 0.27, user: 0.18, sys: 0.09, mem: 345752 ko)
COQNATIVE theories/Data/Member.vo
Warning, feedback message received but no listener to handle it!
Warning: Deprecated environment variable COQLIB, use ROCQLIB instead.
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]Warning, feedback message received but no listener to handle it!
Deprecated environment variable COQLIB, use ROCQLIB instead.
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
Deprecated environment variable COQCORELIB, use ROCQRUNTIMELIB instead.
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
File "./theories/Data/List.v", line 156, characters 2-10:
Error:
Universes
ExtLib.Data.List.234
ExtLib.Data.List.229
ExtLib.Data.List.224
ExtLib.Data.List.219
are unbound.

Command exited with non-zero status 1
theories/Data/List.vo (real: 0.40, user: 0.31, sys: 0.09, mem: 444572 ko)
make[2]: *** [Makefile.coq:813: theories/Data/List.vo] Error 1
make[2]: *** [theories/Data/List.vo] Deleting file 'theories/Data/List.glob'
make[2]: *** Waiting for unfinished jobs....
theories/Data/Member.vo.native (real: 0.30, user: 0.22, sys: 0.07, mem: 62508 ko)
make[1]: *** [Makefile.coq:411: all] Error 2
make[1]: Leaving directory '/github/workspace/builds/coq/coq-failing/_build_ci/ext_lib'
make: *** [Makefile:8: theories] Error 2
+ code=2
+ printf '\n%s exit code: %s\n' ext_lib 2
+ '[' ext_lib '!=' stdlib_test ']'
+ echo 'Aggregating timing log...'
Aggregating timing log...
+ echo

+ tools/make-one-time-file.py --real ext_lib.log
    Time |  Peak Mem | File Name            
--------------------------------------------
0m00.97s | 444572 ko | Total Time / Peak Mem
--------------------------------------------
0m00.40s | 444572 ko | Data/List.vo         
0m00.30s |  62508 ko | Data/Member.vo.native
0m00.27s | 345752 ko | Data/Member.vo       
+ '[' '' ']'
+ exit 2
/github/workspace/builds/coq /github/workspace
::endgroup::

📜 🔎 Minimization Log (truncated to last 8.0KiB; full 505KiB file on GitHub Actions Artifacts under bug.log)

ce; trying one at a time.
Admitting Qeds unsuccessful.
No successful changes.

I will now attempt to remove goals ending in [Abort.]
�[92m
Aborted removal successful.�[0m

I will now attempt to remove unused Ltacs
�[92m
Ltac removal successful.�[0m

I will now attempt to remove unused definitions
�[92m
Definition removal successful.�[0m

I will now attempt to remove unused non-instance, non-canonical structure definitions
�[92m
Non-instance definition removal successful.�[0m

I will now attempt to remove unused variables
�[92m
Variable removal successful.�[0m

I will now attempt to remove unused contexts
�[92m
Context removal successful.�[0m

I will now attempt to admit [abstract ...]s

Non-fatal error: Failed to [abstract ...] admits and preserve the error.  
The new error was:
Deprecated environment variable COQCORELIB, use ROCQRUNTIMELIB instead.
Warning: Deprecated environment variable COQCORELIB,
use ROCQRUNTIMELIB instead.
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
File "/tmp/tmpcdx4hakb/ExtLib/Data/List.v", line 32, characters 2-10:
Error:  (in proof wf_R_list_len): Attempt to save an incomplete proof
(the proof term is not complete because of given up (admitted) goals).
If this is really what you want to do, use Admitted in place of Qed.


�[93mIntermediate code not saved.�[0m

Non-fatal error: Failed to [abstract ...] admits and preserve the error.  
The new error was:
Deprecated environment variable COQCORELIB, use ROCQRUNTIMELIB instead.
Warning: Deprecated environment variable COQCORELIB,
use ROCQRUNTIMELIB instead.
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
File "/tmp/tmpcdx4hakb/ExtLib/Data/List.v", line 32, characters 2-10:
Error:  (in proof wf_R_list_len): Attempt to save an incomplete proof
(the proof term is not complete because of given up (admitted) goals).
If this is really what you want to do, use Admitted in place of Qed.


�[93mIntermediate code not saved.�[0m
Admitting [abstract ...] unsuccessful.
Admitting [abstract ...] unsuccessful.

I will now attempt to remove goals ending in [Abort.]
�[92m
Aborted removal successful.�[0m

I will now attempt to remove unused Ltacs
�[92m
Ltac removal successful.�[0m

I will now attempt to remove unused definitions
�[92m
Definition removal successful.�[0m

I will now attempt to remove unused non-instance, non-canonical structure definitions
�[92m
Non-instance definition removal successful.�[0m

I will now attempt to remove unused variables
�[92m
Variable removal successful.�[0m

I will now attempt to remove unused contexts
�[92m
Context removal successful.�[0m

I will now attempt to replace Obligation with Admit Obligations
�[92m
Admitting Obligations successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting Obligations unsuccessful.
No successful changes.

I will now attempt to admit lemmas with Admitted
�[92m
Admitting lemmas successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting lemmas unsuccessful.
No successful changes.

I will now attempt to admit definitions with Admitted

Non-fatal error: Failed to admit definitions and preserve the error.  
The new error was:
Deprecated environment variable COQCORELIB, use ROCQRUNTIMELIB instead.
Warning: Deprecated environment variable COQCORELIB,
use ROCQRUNTIMELIB instead.
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
Error: The module Nat needs to be closed.


�[93mIntermediate code not saved.�[0m
Failed to do everything at once; trying one at a time.
Admitting definitions unsuccessful.
No successful changes.

I will now attempt to admit lemmas with admit. Defined
�[92m
Admitting lemmas successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting lemmas unsuccessful.
No successful changes.

I will now attempt to admit definitions with admit. Defined

Non-fatal error: Failed to admit definitions and preserve the error.  
The new error was:
Deprecated environment variable COQCORELIB, use ROCQRUNTIMELIB instead.
Warning: Deprecated environment variable COQCORELIB,
use ROCQRUNTIMELIB instead.
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
File "/tmp/tmp797rf9il/ExtLib/Data/List.v", line 16, characters 0-8:
Error:  (in proof wf_R_list_len): Attempt to save an incomplete proof
(the proof term is not complete because of given up (admitted) goals).
If this is really what you want to do, use Admitted in place of Qed.


�[93mIntermediate code not saved.�[0m
Failed to do everything at once; trying one at a time.
Admitting definitions unsuccessful.
No successful changes.

I will now attempt to admit lemmas with Admitted with Proof using
�[92m
Admitting lemmas successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting lemmas unsuccessful.
No successful changes.

I will now attempt to admit definitions with Admitted with Proof using

Non-fatal error: Failed to admit definitions and preserve the error.  
The new error was:
Deprecated environment variable COQCORELIB, use ROCQRUNTIMELIB instead.
Warning: Deprecated environment variable COQCORELIB,
use ROCQRUNTIMELIB instead.
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
Error: The module Nat needs to be closed.


�[93mIntermediate code not saved.�[0m
Failed to do everything at once; trying one at a time.
Admitting definitions unsuccessful.
No successful changes.

I will now attempt to admit lemmas with admit. Defined with Proof using
�[92m
Admitting lemmas successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting lemmas unsuccessful.
No successful changes.

I will now attempt to admit definitions with admit. Defined with Proof using

Non-fatal error: Failed to admit definitions and preserve the error.  
The new error was:
Deprecated environment variable COQCORELIB, use ROCQRUNTIMELIB instead.
Warning: Deprecated environment variable COQCORELIB,
use ROCQRUNTIMELIB instead.
[deprecated-coq-env-var,deprecated-since-9.0,deprecated,default]
File "/tmp/tmp797rf9il/ExtLib/Data/List.v", line 16, characters 0-8:
Error:  (in proof wf_R_list_len): Attempt to save an incomplete proof
(the proof term is not complete because of given up (admitted) goals).
If this is really what you want to do, use Admitted in place of Qed.


�[93mIntermediate code not saved.�[0m
Failed to do everything at once; trying one at a time.
Admitting definitions unsuccessful.
No successful changes.

I will now attempt to add Proof using lines
�[92m
Adding Proof using lines successful.�[0m
Failed to do everything at once; trying one at a time.
Adding Proof using lines unsuccessful.
No successful changes.

I will now attempt to export modules
Module exportation unsuccessful.

I will now attempt to split imports and exports
Import/Export splitting unsuccessful.

I will now attempt to split := definitions
One-line definition splitting unsuccessful.

I will now attempt to remove all lines, one at a time
Line removal unsuccessful.

I will now attempt to remove goals ending in [Abort.]
�[92m
Aborted removal successful.�[0m

I will now attempt to remove unused Ltacs
�[92m
Ltac removal successful.�[0m

I will now attempt to remove unused definitions
�[92m
Definition removal successful.�[0m

I will now attempt to remove unused non-instance, non-canonical structure definitions
�[92m
Non-instance definition removal successful.�[0m

I will now attempt to remove unused variables
�[92m
Variable removal successful.�[0m

I will now attempt to remove unused contexts
�[92m
Context removal successful.�[0m

I will now attempt to remove modules
�[92m
Module removal successful.�[0m
Failed to do everything at once; trying one at a time.
Module removal unsuccessful.
No successful changes.

I will now attempt to remove sections
�[92m
Section removal successful.�[0m
Failed to do everything at once; trying one at a time.
Section removal unsuccessful.
No successful changes.

I will now attempt to remove empty sections

No empty sections to remove.

I will now attempt to remove the admit tactic header

No admit tactic header to remove

Now, I will attempt to strip repeated newlines and trailing spaces from this file...

No strippable newlines or spaces.

If you have any comments on your experience of the minimizer, please share them in a reply (possibly tagging @JasonGross).
If you believe there's a bug in the bug minimizer, please report it on the bug minimizer issue tracker.

tabareau · 2025-09-29T17:27:30Z

@coqbot run full ci

tabareau · 2025-09-29T18:55:38Z

@coqbot run full ci

tabareau · 2025-09-29T19:37:11Z

@coqbot run full ci

jfehrle · 2025-09-30T06:03:52Z

What is "J"? Perhaps you could add some documentation and explain the benefit to users in basic terms. Offhand I can't tell whether this has broad benefits for users or if it's very specialized.

JasonGross · 2025-09-30T06:31:13Z

J is the name of the induction principle for eq (also known as I or Id or the Identity type) in the academic literature. This pr makes rewriting more general (for example, I believe without it, eq must be an inductive type, whereas with this pr, it can be an axiom or module parameter)

tabareau · 2025-09-30T07:14:12Z

@jfehrle I will explain more when the PR will be ready, but one point is also to stop relying on internal_rew like scheme that were generated under the hood for dependent rewriting by the rewrite tactic. And also it allows to use rewrite for other kind of equality, like observational or cubical one. After this PR; I will also use this mechanism to extend ssreflect rewrite and setoid-rewrite.

Zimmi48 · 2025-09-30T09:00:44Z

I will explain more when the PR will be ready

Marking the PR as draft, given that it is not ready yet.

tabareau · 2025-09-30T10:11:21Z

@coqbot run full ci

tabareau requested review from a team as code owners September 19, 2025 14:40

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 19, 2025

tabareau marked this pull request as draft September 19, 2025 15:05

tabareau force-pushed the sortpoly-equality branch 10 times, most recently from 5d85858 to 04fdca3 Compare September 24, 2025 13:41

coqbot-app bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 24, 2025

tabareau force-pushed the sortpoly-equality branch from 04fdca3 to 9e27b8c Compare September 25, 2025 09:03

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 25, 2025

tabareau force-pushed the sortpoly-equality branch 4 times, most recently from a30387b to 428b37f Compare September 25, 2025 09:46

coqbot-app bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 25, 2025

tabareau marked this pull request as ready for review September 25, 2025 11:58

tabareau requested review from a team as code owners September 25, 2025 11:58

tabareau force-pushed the sortpoly-equality branch from 428b37f to e8c319f Compare September 25, 2025 12:59

github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Sep 29, 2025

tabareau force-pushed the sortpoly-equality branch 2 times, most recently from c448b1e to 2152508 Compare September 29, 2025 16:18

coqbot-app bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels Sep 29, 2025

tabareau added 2 commits September 29, 2025 19:08

add a generic mechanism for rewriting with any equality satisfying J

b903e53

make eq_Has_J_r_elim pass guard condition

8c0a681

tabareau force-pushed the sortpoly-equality branch from 2152508 to 8c0a681 Compare September 29, 2025 17:08

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 29, 2025

coqbot-app bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 29, 2025

avoid sort poly instance for backward compat

feabe4c

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 29, 2025

coqbot-app bot added needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. and removed needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Sep 29, 2025

fix output

6f2a108

tabareau force-pushed the sortpoly-equality branch from 3b4944d to 6f2a108 Compare September 29, 2025 19:29

coqbot-app bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 29, 2025

Zimmi48 marked this pull request as draft September 30, 2025 09:00

start fixing ci

5054649

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 30, 2025

coqbot-app bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 30, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Add a generic mechanism for rewriting with any equality satisfying J #21098

Add a generic mechanism for rewriting with any equality satisfying J #21098

tabareau commented Sep 19, 2025

Uh oh!

ppedrot commented Sep 24, 2025

Uh oh!

tabareau commented Sep 25, 2025

Uh oh!

coqbot-app bot commented Sep 29, 2025

Uh oh!

tabareau commented Sep 29, 2025

Uh oh!

tabareau commented Sep 29, 2025

Uh oh!

tabareau commented Sep 29, 2025

Uh oh!

jfehrle commented Sep 30, 2025

Uh oh!

JasonGross commented Sep 30, 2025

Uh oh!

tabareau commented Sep 30, 2025

Uh oh!

Zimmi48 commented Sep 30, 2025

Uh oh!

tabareau commented Sep 30, 2025

Uh oh!

Uh oh!

Add a generic mechanism for rewriting with any equality satisfying J #21098

Are you sure you want to change the base?

Add a generic mechanism for rewriting with any equality satisfying J #21098

Conversation

tabareau commented Sep 19, 2025

Uh oh!

ppedrot commented Sep 24, 2025

Uh oh!

tabareau commented Sep 25, 2025

Uh oh!

coqbot-app bot commented Sep 29, 2025

Uh oh!

tabareau commented Sep 29, 2025

Uh oh!

tabareau commented Sep 29, 2025

Uh oh!

tabareau commented Sep 29, 2025

Uh oh!

jfehrle commented Sep 30, 2025

Uh oh!

JasonGross commented Sep 30, 2025

Uh oh!

tabareau commented Sep 30, 2025

Uh oh!

Zimmi48 commented Sep 30, 2025

Uh oh!

tabareau commented Sep 30, 2025

Uh oh!

Uh oh!