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 /pretyping/evd.mli |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'pretyping/evd.mli')
-rw-r--r-- | pretyping/evd.mli | 57 |
1 files changed, 57 insertions, 0 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli new file mode 100644 index 00000000..f66667aa --- /dev/null +++ b/pretyping/evd.mli @@ -0,0 +1,57 @@ +(************************************************************************) +(* 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: evd.mli,v 1.3.2.1 2004/07/16 19:30:44 herbelin Exp $ i*) + +(*i*) +open Names +open Term +open Sign +(*i*) + +(* The type of mappings for existential variables. + The keys are integers and the associated information is a record + containing the type of the evar ([evar_concl]), the context under which + it was introduced ([evar_hyps]) and its definition ([evar_body]). + [evar_info] is used to add any other kind of information. *) + +type evar = existential_key + +type evar_body = + | Evar_empty + | Evar_defined of constr + +type evar_info = { + evar_concl : constr; + evar_hyps : named_context; + evar_body : evar_body} + +type evar_map + +val empty : evar_map + +val add : evar_map -> evar -> evar_info -> evar_map + +val dom : evar_map -> evar list +val map : evar_map -> evar -> evar_info +val rmv : evar_map -> evar -> evar_map +val remap : evar_map -> evar -> evar_info -> evar_map +val in_dom : evar_map -> evar -> bool +val to_list : evar_map -> (evar * evar_info) list + +val define : evar_map -> evar -> constr -> evar_map + +val non_instantiated : evar_map -> (evar * evar_info) list +val is_evar : evar_map -> evar -> bool + +val is_defined : evar_map -> evar -> bool + +val evar_body : evar_info -> evar_body + +val string_of_existential : evar -> string +val existential_of_int : int -> evar |