Sign in
Join now
coq
stepbrobd.com
/
Star
Starred
Star
1
Something went wrong. Try again.
Fork
0
Eye filled
Watch
Watching
Watch
forked from coq/coq
Star
Starred
Star
1
Something went wrong. Try again.
Fork
0
Eye filled
Watch
Watching
Watch
Overview
Overview
Issues
Issues
Pulls
Pulls
Pipelines
Pipelines
Version history of
kernel/
rtree.ml
March 2026
coqbot-app[bot]
226bb69a
Copied
Failed
Copy SHA
Merge PR #21666: Use automata rather than regular trees for guard
checking.
checking.
Copy SHA
Browse repository
committed
8mo ago
Pierre-Marie Pédrot
1cdafe40
Copied
Failed
Copy SHA
Store inductive automata next to their regular tree in
Declarations.
Declarations.
Copy SHA
Browse repository
committed
8mo ago
Pierre-Marie Pédrot
2f6d51bb
Copied
Failed
Copy SHA
Use automata rather than regular trees for guard
checking.
checking.
Copy SHA
Browse repository
committed
8mo ago
October 2024
coqbot-app[bot]
15e243e6
Copied
Failed
Copy SHA
Merge PR #19692: Update the OCaml headers to reflect the fact Coq is now
Rocq.
Rocq.
Copy SHA
Browse repository
committed
2y ago
Pierre-Marie Pédrot
0bdc010c
Copied
Failed
Copy SHA
Update the OCaml headers to reflect the fact Coq is now
Rocq.
Rocq.
Copy SHA
Browse repository
committed
2y ago
coqbot-app[bot]
52249630
Copied
Failed
Copy SHA
Merge PR #19669: More efficient computation of recursive
trees
trees
Copy SHA
Browse repository
committed
2y ago
Pierre-Marie Pédrot
a937cc15
Copied
Failed
Copy SHA
Introduce a delayed view of recursive trees.
Copy SHA
Browse repository
committed
2y ago
Pierre-Marie Pédrot
e722bc63
Copied
Failed
Copy SHA
Delay expansion of subnodes as late as possible in
Rtree.
Rtree.
Copy SHA
Browse repository
committed
2y ago
Pierre-Marie Pédrot
d10fe4a5
Copied
Failed
Copy SHA
Reimplement Rtree substitution using Esubst module.
Copy SHA
Browse repository
committed
2y ago
Pierre-Marie Pédrot
993b4c28
Copied
Failed
Copy SHA
Move the Rtree module from lib/ to kernel/.
Copy SHA
Browse repository
committed
2y ago
