diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /library/impargs.mli |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'library/impargs.mli')
-rw-r--r-- | library/impargs.mli | 69 |
1 files changed, 69 insertions, 0 deletions
diff --git a/library/impargs.mli b/library/impargs.mli new file mode 100644 index 00000000..8db04ee7 --- /dev/null +++ b/library/impargs.mli @@ -0,0 +1,69 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: impargs.mli,v 1.26.2.1 2004/07/16 19:30:35 herbelin Exp $ i*) + +(*i*) +open Names +open Libnames +open Term +open Environ +open Nametab +(*i*) + +(*s Implicit arguments. Here we store the implicit arguments. Notice that we + 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 is_strict_implicit_args : unit -> bool +val is_contextual_implicit_args : unit -> bool + +type implicits_flags +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 *) +type implicit_status +type implicits_list = implicit_status list + +val is_status_implicit : implicit_status -> bool +val is_inferable_implicit : bool -> int -> implicit_status -> bool +val name_of_implicit : implicit_status -> identifier + +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 : 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 -> + Topconstr.explicitation list -> unit + +(* 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 + +(* For translator *) +val implicits_of_global_out : global_reference -> implicits_list +val is_implicit_args_out : unit -> bool |