Skip to content

Activity

Showing most recent first

make hint extern name a separate object

Force push
jfehrleforce pushed to hint_extern_name • 5cde64d…6ce0c30 • 
on Feb 16

make hint extern name a separate object

Force push
jfehrleforce pushed to hint_extern_name • 6c55804…5cde64d • 
on Feb 7

make hint extern name a separate object

jfehrlepushed 1 commit to hint_extern_name • 73a8620…6c55804 • 
on Feb 7

Try to get correct types for declare_object

jfehrlepushed 1 commit to hint_extern_name • 244b76b…73a8620 • 
on Jan 23

Use a new namespace for Hint Extern names

Force push
jfehrleforce pushed to hint_extern_name • 23e65bb…244b76b • 
on Jan 22

Use a new namespace for Hint Extern names

jfehrlepushed 1 commit to hint_extern_name • 71f851f…23e65bb • 
on Jan 22

Describe info_auto limitations

Force push
jfehrleforce pushed to hintdb_doc • 0646d6c…25a24d9 • 
on Jan 15

Describe info_auto limitations

Force push
jfehrleforce pushed to hintdb_doc • 6d68d1c…0646d6c • 
on Jan 13

Describe info_auto limitations

Force push
jfehrleforce pushed to hintdb_doc • 2140a8a…6d68d1c • 
on Jan 13

Describe info_auto limitations

Force push
jfehrleforce pushed to hintdb_doc • 310d9f2…2140a8a • 
on Jan 12

Describe info_auto limitations

Force push
jfehrleforce pushed to hintdb_doc • 90ac0ed…310d9f2 • 
on Jan 12

Describe info_auto limitations

Force push
jfehrleforce pushed to hintdb_doc • 550b6cf…90ac0ed • 
on Jan 12

Bump version

jfehrlepushed 1 commit to debug_pl_8_19 • 0ebc4cd…c72872c • 
on Nov 30, 2024

Don't enter debugger if no current proof + Interrupt fixes

jfehrlepushed 1 commit to debug_pl_8_19 • fa95a36…0ebc4cd • 
on Nov 30, 2024

Describe info_auto limitations

Force push
jfehrleforce pushed to hintdb_doc • 878a08a…550b6cf • 
on Nov 28, 2024

Reverse bad change to exception in Ltac debugger in rocq-prover#19314

Force push
jfehrleforce pushed to debugger_exn_fix • e72c54d…676044c • 
on Nov 22, 2024

Describe info_auto limitations

jfehrlepushed 1 commit to hintdb_doc • b1323a3…878a08a • 
on Nov 21, 2024

Reverse bad change to exception in Ltac debugger in rocq-prover#19314

Force push
jfehrleforce pushed to debugger_exn_fix • 18e7d75…e72c54d • 
on Nov 20, 2024

Reverse bad change to exception in Ltac debugger in rocq-prover#19314

jfehrlecreated debugger_exn_fix • 18e7d75 • 
on Nov 20, 2024

Refine Hint Opaque/Transparent doc

Force push
jfehrleforce pushed to hintdb_doc • 4eaf5eb…b1323a3 • 
on Nov 18, 2024

Refine Hint Opaque/Transparent doc

Force push
jfehrleforce pushed to hintdb_doc • a419ba3…4eaf5eb • 
on Nov 15, 2024

Refine Hint Opaque/Transparent doc

Force push
jfehrleforce pushed to hintdb_doc • a4a06ab…a419ba3 • 
on Nov 14, 2024

Show "autoapply" for tc eauto; include dbnames in tactic for info where

Force push
jfehrleforce pushed to tce_autoapply • a04df25…a47c088 • 
on Nov 10, 2024

Let users specify a hint name on Hint Extern

Force push
jfehrleforce pushed to hint_extern_name • 5a9679b…71f851f • 
on Nov 10, 2024

Let users specify a hint name on Hint Extern

Force push
jfehrleforce pushed to hint_extern_name • 3138184…5a9679b • 
on Nov 10, 2024

Show "autoapply" for tc eauto; include dbnames in tactic for info where

Force push
jfehrleforce pushed to tce_autoapply • 7382865…a04df25 • 
on Nov 10, 2024

Let users specify a hint name on Hint Extern

Force push
jfehrleforce pushed to hint_extern_name • a92bd71…3138184 • 
on Nov 10, 2024

Show "autoapply" for tc eauto; include dbnames in tactic for info where

jfehrlecreated hint_extern_name • a92bd71 • 
on Nov 10, 2024

Show "autoapply" for tc eauto; include dbnames in tactic for info where

Force push
jfehrleforce pushed to tce_autoapply • 5c1692e…7382865 • 
on Nov 10, 2024

Show "autoapply" for tc eauto; include dbnames in tactic for info where

Force push
jfehrleforce pushed to tce_autoapply • b6a167a…5c1692e • 
on Nov 10, 2024