diff options
| author | herbelin | 2000-10-18 17:51:58 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-18 17:51:58 +0000 |
| commit | edfda2501f08f18e24bd2e3eca763eb1c2dec0ea (patch) | |
| tree | e4c42c670c2f61b95a7a0f68fd96f635aeef8b2b /kernel/sign.mli | |
| parent | a586cb418549eb523a3395155cab2560fd178571 (diff) | |
Simplifications autour de typed_type (renommé types par analogie avec sorts); documentation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@727 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/sign.mli')
| -rw-r--r-- | kernel/sign.mli | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/kernel/sign.mli b/kernel/sign.mli index 51e8107448..29edde8f6b 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -12,12 +12,12 @@ open Term type named_context = named_declaration list val add_named_decl : - identifier * constr option * typed_type -> named_context -> named_context -val add_named_assum : identifier * typed_type -> named_context -> named_context + identifier * constr option * types -> named_context -> named_context +val add_named_assum : identifier * types -> named_context -> named_context val add_named_def : - identifier * constr * typed_type -> named_context -> named_context -val lookup_id : identifier -> named_context -> constr option * typed_type -val lookup_id_type : identifier -> named_context -> typed_type + identifier * constr * types -> named_context -> named_context +val lookup_id : identifier -> named_context -> constr option * types +val lookup_id_type : identifier -> named_context -> types val lookup_id_value : identifier -> named_context -> constr option val pop_named_decl : identifier -> named_context -> named_context val empty_named_context : named_context @@ -41,12 +41,12 @@ val keep_hyps : Idset.t -> named_context -> named_context type rel_context = rel_declaration list -val add_rel_decl : (name * constr option * typed_type) -> rel_context -> rel_context -val add_rel_assum : (name * typed_type) -> rel_context -> rel_context -val add_rel_def : (name * constr * typed_type) -> rel_context -> rel_context -val lookup_rel_type : int -> rel_context -> name * typed_type +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 +val lookup_rel_type : int -> rel_context -> name * types val lookup_rel_value : int -> rel_context -> constr option -val lookup_rel_id : identifier -> rel_context -> int * typed_type +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 |