Réorganisation de Impargs + mise en place d'une infrastructure

(notatemment des tables de parsing et d'affichage différenciées)
permettant au traducteur de changer les implicites


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

1 files changed, 18 insertions, 21 deletions

diff --git a/library/impargs.mli b/library/impargs.mli
index 09462ea23..a9f57e288 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -20,12 +20,16 @@ open Nametab
     are outside the kernel, which knows nothing about implicit arguments. *)
 
 val make_implicit_args : bool -> unit
+val make_strict_implicit_args : bool -> unit
+val make_contextual_implicit_args : bool -> unit
+
 val is_implicit_args : unit -> bool
-val implicitly : ('a -> 'b) -> 'a -> 'b
-val with_implicits : bool -> ('a -> 'b) -> 'a -> 'b
+val is_strict_implicit_args : unit -> bool
+val is_contextual_implicit_args : unit -> bool
 
-val strict_implicit_args : bool ref
-val contextual_implicit_args : bool ref
+type implicits_flags
+val implicitly : ('a -> 'b) -> 'a -> 'b
+val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b
 
 (*s An [implicits_list] is a list of positions telling which arguments
     of a reference can be automatically infered *)
@@ -38,34 +42,27 @@ val positions_of_implicits : implicits_list -> int list
 
 (* Computation of the positions of arguments automatically inferable
    for an object of the given type in the given env *)
-val compute_implicits : env -> types -> implicits_list
+val compute_implicits : bool -> env -> types -> implicits_list
 
 (*s Computation of implicits (done using the global environment). *)
 
 val declare_var_implicits : variable -> unit
 val declare_constant_implicits : constant -> unit
 val declare_mib_implicits : mutual_inductive -> unit
+
 val declare_implicits : global_reference -> unit
 
 (* Manual declaration of which arguments are expected implicit *)
 val declare_manual_implicits : global_reference -> int list -> unit
 
-(*s Access to already computed implicits. *)
-
-val constructor_implicits_list : constructor -> implicits_list
-val inductive_implicits_list : inductive -> implicits_list
-val constant_implicits_list : constant -> implicits_list
-
-val implicits_of_var : variable -> implicits_list
-
-val is_implicit_constant : constant -> bool
-val is_implicit_inductive_definition : inductive -> bool
-val is_implicit_var : variable -> bool
+(* Get implicit arguments *)
+val is_implicit_constant : constant -> implicits_flags
+val is_implicit_inductive_definition : mutual_inductive -> implicits_flags
+val is_implicit_var : variable -> implicits_flags
 
 val implicits_of_global : global_reference -> implicits_list
 
-(*s Rollback. *)
-
-type frozen_t
-val freeze : unit -> frozen_t
-val unfreeze : frozen_t -> unit
+(* For translator *)
+val implicits_of_global_out : global_reference -> implicits_list
+val is_implicit_args_out : unit -> bool
+val set_var_implicits : variable -> implicits_list -> unit