From 0dd3f0d34873dcd126be8ec48724a310214f38ac Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 9 Sep 2014 22:39:15 +0200
Subject: - Fix printing and parsing of primitive projections, including the
 Set Printing All cases (bug #3597). - Fix Ltac matching with primitive
 projections (bug #3598). - Spotted a problem with printing of constants with
 maximally implicit arguments due to strange "compatibility" interpretation of
 Arguments [X] as Arguments {X} but didn't fix it entirely yet (might cause
 incompatibilities).

---
 library/impargs.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/impargs.ml b/library/impargs.ml
index 55e21b2c8c..355cbe1fa8 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -378,7 +378,9 @@ let set_manual_implicits env flags enriching autoimps l =
           l, imp, m
       in
       let imps' = merge (k+1) l' imps in
-      let m = Option.map (fun (b,f) -> set_maximality imps' b, f) m in
+      let m = Option.map (fun (b,f) -> 
+	(* match imp with Some Manual -> (b,f) *)
+	(* | _ ->  *)set_maximality imps' b, f) m in
       Option.map (set_implicit id imp) m :: imps'
   | (Anonymous,imp)::imps ->
       let l', forced = try_forced k l in
-- 
cgit v1.2.3