suppression de Fw pour les implicites

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@405 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 8 insertions, 8 deletions

diff --git a/library/declare.ml b/library/declare.ml
index f186aa18c4..2a9dc279cb 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -269,7 +269,7 @@ let global_reference_imps kind id =
     | DOPN (MutConstruct ((sp,i),j),_) ->
 	c, list_of_implicits (constructor_implicits ((sp,i),j))
     | VAR id ->
-	c, implicits_of_var kind id
+	c, implicits_of_var id
     | _ -> assert false
 
 let global env id =
diff --git a/library/impargs.ml b/library/impargs.ml
index d53d576fbe..06ce6915be 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -101,7 +101,7 @@ let declare_var_implicits id =
   let imps = auto_implicits (body_of_type ty) in
   var_table := Idmap.add id imps !var_table
 
-let implicits_of_var _ id =
+let implicits_of_var id =
   list_of_implicits (try Idmap.find id !var_table with Not_found -> No_impl)
 
 (* Registration as global tables and roolback. *)
diff --git a/library/impargs.mli b/library/impargs.mli
index 243eb8031c..8af10d7ec9 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -34,7 +34,7 @@ val inductive_implicits_list : inductive_path -> int list
 val constant_implicits_list : section_path -> int list
 
 val declare_var_implicits : identifier -> unit
-val implicits_of_var : Names.path_kind -> identifier -> int list
+val implicits_of_var : identifier -> int list
 
 type frozen_t
 val freeze : unit -> frozen_t
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 4bef9a0eb9..bdb0f17138 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -156,7 +156,7 @@ let dbize_ref k sigma env loc s =
   try 
     match lookup_id id env with
       | RELNAME(n,_) -> RRef (loc,RVar id),[]
-      | _ -> RRef(loc,RVar id), (try implicits_of_var k id with _ -> [])
+      | _ -> RRef(loc,RVar id), (try implicits_of_var id with _ -> [])
   with Not_found ->
     try 
       let c,il = match k with
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 19773d6869..641fa40356 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -223,7 +223,7 @@ let print_extracted_mutual sp =
 
 let print_variable sp =
   let (name,typ,_,_) = out_variable sp in
-  let l = implicits_of_var (kind_of_path sp) name in
+  let l = implicits_of_var name in
   [< print_var (string_of_id name) typ; print_impl_args l; 'fNL >]
 
 let print_constant with_values sep sp =
@@ -453,7 +453,7 @@ let print_name name =
 	      | VAR _ ->
 		  let (_,typ) = Global.lookup_var name in 
 		  [< print_var str typ;
-		     try print_impl_args (implicits_of_var CCI name)
+		     try print_impl_args (implicits_of_var name)
 		     with _ -> [<>] >]
 	      | DOPN(Const sp,_) ->
 		  print_constant true " = " sp
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 183c015eae..ce180ba1c7 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -174,7 +174,7 @@ let implicit_of_ref = function
   | RConstruct (cstrid,_) -> constructor_implicits_list cstrid
   | RInd (indid,_) -> inductive_implicits_list indid
   | RConst (sp,_) -> constant_implicits_list sp
-  | RVar id -> (try (implicits_of_var CCI id) with _ -> []) (* et FW? *)
+  | RVar id -> (try (implicits_of_var id) with _ -> []) (* et FW? *)
   | _ -> []
 
 let rec skip_coercion dest_ref (f,args as app) =
@@ -452,7 +452,7 @@ let bdize_app c al =
       | DOPN(MutConstruct constr_sp,_) -> constructor_implicits_list constr_sp
       | DOPN(MutInd ind_sp,_) -> inductive_implicits_list ind_sp
       | DOPN(Const sp,_) -> constant_implicits_list sp
-      | VAR id -> (try (implicits_of_var CCI id) with _ -> []) (* et FW? *)
+      | VAR id -> (try implicits_of_var id with _ -> []) (* et FW? *)
       | _ -> []
   in
   if !print_implicits then