diff options
| author | filliatr | 1999-10-14 09:35:03 +0000 |
|---|---|---|
| committer | filliatr | 1999-10-14 09:35:03 +0000 |
| commit | ba055245dc4a5de2c4ad6bc8b3a2d20dbeaeb135 (patch) | |
| tree | 5e267e3fdb4922872eca052fff67b1e9c5806966 /kernel/evd.mli | |
| parent | 825775bf4950e1022c18ddd8477563b7510f54a4 (diff) | |
module Proof_trees
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@104 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/evd.mli')
| -rw-r--r-- | kernel/evd.mli | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/kernel/evd.mli b/kernel/evd.mli index fa60292836..89cefcab11 100644 --- a/kernel/evd.mli +++ b/kernel/evd.mli @@ -10,7 +10,8 @@ open Sign (* The type of mappings for existential variables. The keys are integers and the associated information is a record containing the type of the evar ([concl]), the signature under which - it was introduced ([hyps]) and its definition ([body]). *) + it was introduced ([hyps]) and its definition ([body]). + [evar_info] is used to add any other kind of information. *) type evar = int @@ -21,12 +22,14 @@ type evar_body = | Evar_defined of constr type evar_info = { - evar_concl : typed_type; - evar_hyps : typed_type signature; - evar_body : evar_body } + evar_concl : constr; + evar_hyps : typed_type signature; + evar_body : evar_body } type 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 @@ -35,9 +38,6 @@ val in_dom : evar_map -> evar -> bool val to_list : evar_map -> (evar * evar_info) list val mt_evd : evar_map -val add_with_info : evar_map -> evar -> evar_info -> evar_map -val add_noinfo : - evar_map -> evar -> typed_type signature -> typed_type -> evar_map val define : evar_map -> evar -> constr -> evar_map |