From 837bc87ebb180e47e52bef68925568b250dc60ee Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 1 Jun 2009 18:45:08 +0000
Subject: Prevent automatic inference of implicit arguments when the auto flag
 is not set.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12155 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/impargs.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/library/impargs.ml b/library/impargs.ml
index b4b61461f4..96c5c2a5c4 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -308,9 +308,9 @@ let const v _ = v
 let compute_implicits_auto env f manual t =
   match manual with
   | [] -> 
-      let l = compute_implicits_flags env f false t in
-	if not f.auto then List.map (const None) l
-	else prepare_implicits f l
+      if not f.auto then []
+      else let l = compute_implicits_flags env f false t in
+	     prepare_implicits f l
   | _ -> compute_manual_implicits env f t f.auto manual
 	
 let compute_implicits env t = compute_implicits_auto env !implicit_args [] t
-- 
cgit v1.2.3