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 /library/impargs.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 'library/impargs.mli')
| -rw-r--r-- | library/impargs.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/library/impargs.mli b/library/impargs.mli index 3ba9285085..297145f09c 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -120,8 +120,6 @@ val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool val implicits_of_global : global_reference -> implicits_list list -val strict_implicits_of_global : int -> global_reference -> bool list - val extract_impargs_data : implicits_list list -> ((int * int) option * implicit_status list) list |