diff options
| author | filliatr | 1999-10-20 20:41:08 +0000 |
|---|---|---|
| committer | filliatr | 1999-10-20 20:41:08 +0000 |
| commit | d18d82c9e58567384ea632c77a5c1531f6d534cb (patch) | |
| tree | 88b97805630eee3205aad0e818030158fbf7903d /kernel/evd.mli | |
| parent | a8972eb35ab1020ed9a379811c372fae53deef41 (diff) | |
- documentation repertoire proofs/
- IsAppL of constr * constr list ==> répercussion
- module Clenv (suite; as terminé)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@113 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/evd.mli')
| -rw-r--r-- | kernel/evd.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/evd.mli b/kernel/evd.mli index df80ee72b7..62378f921e 100644 --- a/kernel/evd.mli +++ b/kernel/evd.mli @@ -10,8 +10,8 @@ open Environ (* 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]). + containing the type of the evar ([evar_concl]), the environment under which + it was introduced ([evar_env]) and its definition ([evar_body]). [evar_info] is used to add any other kind of information. *) type evar = int |