diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-27 22:30:58 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-27 23:37:31 +0100 |
| commit | a9fd21ac2b2e3908d8eb8d5a549c43949cddc69a (patch) | |
| tree | b6e897f501785ccc38df16df854479d0754a92c4 /lib/future.mli | |
| parent | 8ff32fd0748b0d1d7bd0a7612e05c26236b65d48 (diff) | |
Reverting the following block of three commits:
- Registering strict implicit arguments systematically (35fc7d728168)
- Experimenting always forcing convertibility on strict implicit arguments (a1a6d7b99eef5e6)
- Fixing Coq compilation (894a3d16471)
Systematically computing strict implicit arguments can lead to big
computations, so I suspend this attempt, waiting for improved
computation of implicit arguments, or alternative heuristics going
toward having more conversion in rewrite.
Diffstat (limited to 'lib/future.mli')
0 files changed, 0 insertions, 0 deletions