diff options
| author | Hugo Herbelin | 2014-11-27 22:30:58 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-27 23:37:31 +0100 |
| commit | a9fd21ac2b2e3908d8eb8d5a549c43949cddc69a (patch) | |
| tree | b6e897f501785ccc38df16df854479d0754a92c4 /dev | |
| 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 'dev')
| -rw-r--r-- | dev/printers.mllib | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index ec362b5388..2e61cb6973 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -144,7 +144,6 @@ Program Coercion Cases Pretyping -Impargs Unification Declaremods Library |