From af767e36829ada2b23f5d8eae631649e865392ae Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 10 Sep 2014 12:59:44 +0200
Subject: Parsing and printing of primitive projections, fix buggy behavior
 when implicits do not allow to parse as an application and cleanup code.

---
 library/impargs.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'library')

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
-- 
cgit v1.2.3