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 /pretyping/pretyping.mllib | |
| 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 'pretyping/pretyping.mllib')
| -rw-r--r-- | pretyping/pretyping.mllib | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 2958b9e73..b189360c0 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -31,5 +31,4 @@ Detyping Indrec Cases Pretyping -Impargs Unification |