diff options
| author | Matthieu Sozeau | 2014-09-10 12:59:44 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-10 13:01:24 +0200 |
| commit | af767e36829ada2b23f5d8eae631649e865392ae (patch) | |
| tree | fc850ddd224e3f6ed5acd6417d27bb71ff07dcbf /library | |
| parent | 6624459e492164b3d189e3518864379ff985bf8c (diff) | |
Parsing and printing of primitive projections, fix buggy behavior when
implicits do not allow to parse as an application and cleanup code.
Diffstat (limited to 'library')
| -rw-r--r-- | library/impargs.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index 355cbe1fa8..cbbb2cea95 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -410,10 +410,6 @@ let compute_constant_implicits flags manual cst = let ty = Typeops.type_of_constant_type env cb.const_type in let impls = compute_semi_auto_implicits env flags manual ty in impls - (* match cb.const_proj with *) - (* | None -> impls *) - (* | Some {proj_npars = n} -> *) - (* List.map (fun (x,args) -> x, CList.skipn_at_least n args) impls *) (*s Inductives and constructors. Their implicit arguments are stored in an array, indexed by the inductive number, of pairs $(i,v)$ where |