test-suite/complexity · coq · Tangled

forked from coq/coq

coq test-suite complexity

19 files

zimmi48.tngl.sh · Substitute all URLs to renamed repository. · 1y ago

added cached term to congruence encapsulated cached term in module ATerm added complexity test, changelog entry

bug_5702_guard.v

Using strongly wellfounded fixpoints in tests with loops in erasable subterms,

Fixing complexity tests for #4076.

Fixing complexity tests for #4076.

test-suite/complexity/constructor: -native-compiler no

evar_instance.v

Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2). Reasoning modulo variable aliases induced an extra lookup in the environment at each inversion of the components of the evar instances: precomputing the aliases map allowed to gain a factor n. Moreover, solve_evar_evar_l2r was recomputing the evar substitution from the evar instance n more times than needed. Function solve_evar_evar_l2r is still on O(n^2) but it does not seem to be used so often actually. The trivial case has been optimized (linear time) but the general case could probably be also cut down to O(n*log(n)) if needed.

[toplevel] Deprecate the `-compile` flag in favor of `coqc`.

guard_illegal_call.v

[test-suite] Cleanup some stdlib dependencies

guard_return_predicate.v

An optimization in the guard checker.

[test-suite] Cleanup some stdlib dependencies

[impargs] use whd_all from kernel

Fix test-suite fo non maximal implicit arguments

Small things about coqdoc + fixing lettuple.v test (part of bug #2289) In coqdoc, made links to utf8 notations working and made representation of locations for notations more compact

Fixing format of complexity bug Notations.v.

Substitute all URLs to renamed repository.

patternmatching.v

Optimizing the compilation of unused aliases in pattern-matching.

setoid_rewrite.v

Turn to error use of Let/Variable/Hypothesis outside sections

[toplevel] Deprecate the `-compile` flag in favor of `coqc`.