Ré-introduction des implicites à la volée dans la définition des inductifs

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

2 files changed, 27 insertions, 26 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index 3232c4848..2644944ac 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -32,7 +32,7 @@ let add_free_rels_until bound m acc =
 
 (* calcule la liste des arguments implicites *)
 
-let poly_args env sigma t =
+let compute_implicits env sigma t =
   let rec aux env n t =
     match kind_of_term (whd_betadeltaiota env sigma t) with
       | IsProd (x,a,b) ->
@@ -45,9 +45,11 @@ let poly_args env sigma t =
 	Intset.elements (aux (push_rel_assum (x,a) env) 1 b)
     | _ -> []
 
+type implicits_list = int list
+
 type implicits =
-  | Impl_auto of int list
-  | Impl_manual of int list
+  | Impl_auto of implicits_list
+  | Impl_manual of implicits_list
   | No_impl
 
 let implicit_args = ref false
@@ -73,7 +75,7 @@ let using_implicits = function
   | No_impl -> with_implicits false
   | _ -> with_implicits true
 
-let auto_implicits env ty = Impl_auto (poly_args env Evd.empty ty)
+let auto_implicits env ty = Impl_auto (compute_implicits env Evd.empty ty)
 
 let list_of_implicits = function 
   | Impl_auto l -> l
diff --git a/library/impargs.mli b/library/impargs.mli
index bc52caea0..bd5f6024a 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -4,50 +4,49 @@
 (*i*)
 open Names
 open Term
+open Environ
 open Inductive
 (*i*)
 
 (*s Implicit arguments. Here we store the implicit arguments. Notice that we 
     are outside the kernel, which knows nothing about implicit arguments. *)
 
-type implicits =
-  | Impl_auto of int list
-  | Impl_manual of int list
-  | No_impl
-
 val make_implicit_args : bool -> unit
 val is_implicit_args : unit -> bool
 val implicitely : ('a -> 'b) -> 'a -> 'b
 val with_implicits : bool -> ('a -> 'b) -> 'a -> 'b
 
-val list_of_implicits : implicits -> int list
+(*s An [implicits_list] is a list of positions telling which arguments
+    of a reference can be automatically infered *)
+type implicits_list = int list
 
-(*s Computation of implicits (done using the global environment). *)
+(* Computation of the positions of arguments automatically inferable
+   for an object of the given type in the given env *)
+val compute_implicits : env -> 'a Evd.evar_map -> types -> implicits_list
 
-val declare_var_implicits : section_path -> unit
-val declare_constant_implicits : section_path -> unit
-val declare_mib_implicits : section_path -> unit
+(*s Computation of implicits (done using the global environment). *)
 
+val declare_var_implicits : variable_path -> unit
+val declare_constant_implicits : constant_path -> unit
+val declare_mib_implicits : mutual_inductive_path -> unit
 val declare_implicits : global_reference -> unit
-val declare_manual_implicits : global_reference -> int list -> unit
 
-(*s Access to already computed implicits. *)
+(* Manual declaration of which arguments are expected implicit *)
+val declare_manual_implicits : global_reference -> implicits_list -> unit
 
-val constant_implicits : section_path -> implicits
-val inductive_implicits : inductive_path -> implicits
-val constructor_implicits : constructor_path -> implicits
+(*s Access to already computed implicits. *)
 
-val constructor_implicits_list : constructor_path -> int list
-val inductive_implicits_list : inductive_path -> int list
-val constant_implicits_list : section_path -> int list
+val constructor_implicits_list : constructor_path -> implicits_list
+val inductive_implicits_list : inductive_path -> implicits_list
+val constant_implicits_list : constant_path -> implicits_list
 
-val implicits_of_var : section_path -> int list
+val implicits_of_var : variable_path -> implicits_list
 
-val is_implicit_constant : section_path -> bool
+val is_implicit_constant : constant_path -> bool
 val is_implicit_inductive_definition : inductive_path -> bool
-val is_implicit_var : section_path -> bool
+val is_implicit_var : variable_path -> bool
 
-val implicits_of_global : global_reference -> int list
+val implicits_of_global : global_reference -> implicits_list
 
 (*s Rollback. *)