diff options
| author | filliatr | 2000-11-06 16:43:51 +0000 |
|---|---|---|
| committer | filliatr | 2000-11-06 16:43:51 +0000 |
| commit | 723c344d3e4cf7fdc2e4854ea7d55d140570424d (patch) | |
| tree | 41ae18d8e43aa80007d361e83414d3b043f693ee /kernel/safe_typing.mli | |
| parent | 826913ee19c25cfe445f574080524662bdba1597 (diff) | |
nouveau discharge fait par le noyau; plus de recettes dans les corps des constantes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@807 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 89e3fbbb76..011d0e414e 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -31,13 +31,13 @@ val push_named_assum : val push_named_def : identifier * constr -> safe_environment -> safe_environment -val add_constant : - section_path -> constant_entry -> safe_environment -> safe_environment -val add_lazy_constant : - section_path -> (unit -> constr) -> constr -> safe_environment - -> safe_environment val add_parameter : section_path -> constr -> safe_environment -> safe_environment +val add_constant : + section_path -> constant_entry -> safe_environment -> safe_environment +val add_discharged_constant : + section_path -> Cooking.recipe -> safe_environment -> safe_environment + val add_mind : section_path -> mutual_inductive_entry -> safe_environment -> safe_environment @@ -46,13 +46,13 @@ val add_constraints : constraints -> safe_environment -> safe_environment val pop_named_decls : identifier list -> safe_environment -> safe_environment val lookup_named : identifier -> safe_environment -> constr option * types -(*i -val lookup_rel : int -> safe_environment -> name * types -i*) val lookup_constant : section_path -> safe_environment -> constant_body val lookup_mind : section_path -> safe_environment -> mutual_inductive_body val lookup_mind_specif : inductive -> safe_environment -> inductive_instance +val set_opaque : safe_environment -> section_path -> unit +val set_transparent : safe_environment -> section_path -> unit + val export : safe_environment -> string -> compiled_env val import : compiled_env -> safe_environment -> safe_environment |