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 /interp | |
| 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 'interp')
| -rw-r--r-- | interp/interp.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/interp/interp.mllib b/interp/interp.mllib index d3b7077c4b..c9a0315267 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -10,6 +10,7 @@ Dumpglob Syntax_def Smartlocate Reserve +Impargs Implicit_quantifiers Constrintern Modintern |