From 4c9696c6dac1beb1b19fe3bb083dee0b1ef1bd00 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 3 May 2000 18:04:46 +0000
Subject: suppression de Fw pour les implicites

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@405 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/declare.ml  | 2 +-
 library/impargs.ml  | 2 +-
 library/impargs.mli | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'library')

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