diff options
| author | herbelin | 2001-02-14 15:41:55 +0000 |
|---|---|---|
| committer | herbelin | 2001-02-14 15:41:55 +0000 |
| commit | e7d592ada2d681876d2bcf0a45d4267b3746064f (patch) | |
| tree | e0b7eb1e67b1871b7cb356c33f66182f6dde86c3 /kernel/sign.mli | |
| parent | 045c85f66a65c6aaedeed578d352c6de27d5e6a4 (diff) | |
Mise en place d'un système optionnel de discharge immédiat; prise en compte des défs locales dans les arguments des inductifs; nettoyage divers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1381 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/sign.mli')
| -rw-r--r-- | kernel/sign.mli | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/kernel/sign.mli b/kernel/sign.mli index 5c93bccbf3..ede431eb4e 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -36,11 +36,22 @@ val instantiate_sign : val keep_hyps : Idset.t -> named_context -> named_context val instance_from_named_context : named_context -> constr list +(*s Signatures of ordered section variables *) + +type section_declaration = variable_path * constr option * constr +type section_context = section_declaration list + +val instance_from_section_context : section_context -> constr list + (*s Signatures of ordered optionally named variables, intended to be accessed by de Bruijn indices *) +(* In [rel_context], more recent declaration is on top *) type rel_context = rel_declaration list +(* In [rev_rel_context], older declaration is on top *) +type rev_rel_context = rel_declaration list + val add_rel_decl : (name * constr option * types) -> rel_context -> rel_context val add_rel_assum : (name * types) -> rel_context -> rel_context val add_rel_def : (name * constr * types) -> rel_context -> rel_context @@ -50,10 +61,13 @@ val lookup_rel_id : identifier -> rel_context -> int * types val empty_rel_context : rel_context val rel_context_length : rel_context -> int val lift_rel_context : int -> rel_context -> rel_context +val lift_rev_rel_context : int -> rev_rel_context -> rev_rel_context val concat_rel_context : newer:rel_context -> older:rel_context -> rel_context val ids_of_rel_context : rel_context -> identifier list val assums_of_rel_context : rel_context -> (name * constr) list val map_rel_context : (constr -> constr) -> rel_context -> rel_context +val push_named_to_rel_context : named_context -> rel_context -> rel_context +val reverse_rel_context : rel_context -> rev_rel_context (*s This is used to translate names into de Bruijn indices and vice-versa without to care about typing information *) |