Fixed costly general recursive rhs modality instance, partially fixed running...
Fixed costly general recursive rhs modality instance, partially fixed running TC search too often for recursive hint search.
Showing
- theories/biabd/instances_base.v 3 additions, 0 deletionstheories/biabd/instances_base.v
- theories/biabd/search.v 63 additions, 27 deletionstheories/biabd/search.v
- theories/biabd/search_abd.v 38 additions, 26 deletionstheories/biabd/search_abd.v
- theories/examples/comparison/clh_lock.v 1 addition, 1 deletiontheories/examples/comparison/clh_lock.v
- theories/steps/introduce_hyp.v 2 additions, 0 deletionstheories/steps/introduce_hyp.v
- theories/steps/pure_solver.v 3 additions, 2 deletionstheories/steps/pure_solver.v
- theories/steps/tactics.v 6 additions, 6 deletionstheories/steps/tactics.v
- theories/util_classes.v 6 additions, 0 deletionstheories/util_classes.v
- theories/util_instances.v 6 additions, 0 deletionstheories/util_instances.v
Loading
Please register or sign in to comment