diff options
| author | herbelin | 2011-10-10 22:00:04 +0000 |
|---|---|---|
| committer | herbelin | 2011-10-10 22:00:04 +0000 |
| commit | d74f1da437c214cc0c960e87e8bbf04dd214128e (patch) | |
| tree | 017dc70a7db4dc08a1f414aeacec631a47bc91ad /kernel/type_errors.mli | |
| parent | 32bcb10ce3470377314b964223ce9aed1ab33c72 (diff) | |
Passed conv_algo to evar_define and move call to solve_refl to
evar_define so that it can recursively deal with evar/evar problems.
Also, check_evar_instance now called after each instantiation.
Also did a bit of file reformatting.
The commit apparently induces a loss of some 0,4% on the compilation
of the standard library. Maybe, introducing a heuristic to decide when
to call check_evar_instance (which I guess is responsible for the
overhead) might be a good thing to look at?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14534 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions